YES(?, 2537*a + 2537*b + 10484*a*d + 10484*b*d + 10508*a*c + 10508*b*c + 3292*d + 3300*c + 1824*a^2*d + 3648*a*b*d + 1824*a^2*c + 3648*a*b*c + 312*a^2 + 624*a*b + 1824*b^2*d + 1824*b^2*c + 312*b^2 + 3168*a*c*d + 3168*b*c*d + 1632*a*c^2 + 1632*b*c^2 + 544*c*d + 288*c^2 + 2304*a^2*d^2 + 4608*a*b*d^2 + 4608*a^2*c*d + 9216*a*b*c*d + 1536*a*d^2 + 2304*b^2*d^2 + 4608*b^2*c*d + 1536*b*d^2 + 2304*a^2*c^2 + 4608*a*b*c^2 + 2304*b^2*c^2 + 256*d^2 + 815) Initial complexity problem: 1: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (?, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (?, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (?, 1) evalfbb7in(a, b, c, d, e, f) -> evalfreturnin(a, b, c, d, e, f) [ d >= a + 1 ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (?, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) (?, 1) evalfreturnin(a, b, c, d, e, f) -> evalfstop(a, b, c, d, e, f) 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, f) -> evalfentryin(a, b, c, d, e, f) (?, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (?, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (?, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) 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, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (?, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (?, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfstart) = -3*V_1 + 3*V_2 + 1 Pol(evalfentryin) = -3*V_1 + 3*V_2 + 1 Pol(evalfbb7in) = 3*V_1 - 3*V_4 + 1 Pol(evalfbb5in) = 3*V_1 - 3*V_4 Pol(evalfbb1in) = 3*V_1 - 3*V_4 Pol(evalfbb6in) = 3*V_1 - 3*V_4 - 1 Pol(evalfbb3in) = 3*V_1 - 3*V_4 Pol(evalfbb2in) = 3*V_1 - 3*V_4 Pol(evalfbb4in) = 3*V_1 - 3*V_4 orients all transitions weakly and the transition evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] strictly and produces the following problem: 4: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (?, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb6in) = 1 Pol(evalfbb7in) = 0 Pol(evalfbb5in) = 2 Pol(evalfbb1in) = 2 Pol(evalfbb4in) = 2 Pol(evalfbb3in) = 2 Pol(evalfbb2in) = 2 and size complexities S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-0) = b S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-1) = c S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-2) = d S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-3) = ? S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-4) = ? S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-5) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-0) = b S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-1) = c S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-2) = d S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-3) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-4) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-5) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-0) = b S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-1) = c S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-2) = d S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-3) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-4) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-3) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-3) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-5) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-0) = b S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-1) = c S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-2) = d S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-3) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-4) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-3) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-3) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-5) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-0) = b S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-1) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-2) = d S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-3) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-4) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-5) = ? S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-0) = b S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-1) = c S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-2) = d S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-3) = a S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-4) = e S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-5) = f S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f orients the transitions evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) weakly and the transition evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) strictly and produces the following problem: 5: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb5in) = 1 Pol(evalfbb6in) = 0 Pol(evalfbb1in) = 1 Pol(evalfbb4in) = 1 Pol(evalfbb3in) = 1 Pol(evalfbb2in) = 1 and size complexities S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-0) = b S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-1) = c S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-2) = d S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-4) = ? S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-5) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-0) = b S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-1) = c S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-2) = d S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-4) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-5) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-0) = b S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-1) = c S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-2) = d S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-3) = 7*a + 7*b + 98 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-4) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-5) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-0) = b S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-1) = c S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-2) = d S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-3) = 7*a + 7*b + 98 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-4) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-5) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-0) = b S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-1) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-2) = d S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-3) = 7*a + 7*b + 98 S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-4) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-5) = ? S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-0) = b S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-1) = c S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-2) = d S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-3) = a S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-4) = e S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-5) = f S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f orients the transitions evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) weakly and the transition evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] strictly and produces the following problem: 6: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (?, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb5in) = 4*V_3 - 4*V_5 + 1 Pol(evalfbb1in) = 4*V_3 - 4*V_5 Pol(evalfbb4in) = 4*V_3 - 4*V_5 - 2 Pol(evalfbb3in) = 4*V_3 - 4*V_5 - 1 Pol(evalfbb2in) = 4*V_3 - 4*V_5 - 1 and size complexities S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-0) = b S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-1) = c S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-2) = d S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-4) = ? S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-5) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-0) = b S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-1) = c S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-2) = d S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-4) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-5) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-0) = b S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-1) = c S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-2) = d S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-3) = 7*a + 7*b + 98 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-4) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-5) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-0) = b S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-1) = c S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-2) = d S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-3) = 7*a + 7*b + 98 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-4) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-5) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-0) = b S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-1) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-2) = d S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-3) = 7*a + 7*b + 98 S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-4) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-5) = ? S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-0) = b S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-1) = c S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-2) = d S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-3) = a S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-4) = e S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-5) = f S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f orients the transitions evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) weakly and the transition evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] strictly and produces the following problem: 7: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (?, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 Repeatedly propagating knowledge in problem 7 produces the following problem: 8: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (?, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb4in) = 1 Pol(evalfbb5in) = 0 Pol(evalfbb3in) = 2 Pol(evalfbb2in) = 2 and size complexities S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-0) = b S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-1) = c S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-2) = d S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-4) = ? S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-5) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-0) = b S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-1) = c S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-2) = d S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-4) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-5) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-0) = b S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-1) = c S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-2) = d S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-3) = 7*a + 7*b + 98 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-4) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-4) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-5) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-0) = b S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-1) = c S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-2) = d S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-3) = 7*a + 7*b + 98 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-4) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-4) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-5) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-0) = b S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-1) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-2) = d S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-3) = 7*a + 7*b + 98 S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-4) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-5) = ? S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-0) = b S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-1) = c S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-2) = d S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-3) = a S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-4) = e S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-5) = f S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f orients the transitions evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) weakly and the transition evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) strictly and produces the following problem: 9: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 8*c + 6*a + 6*b + 2, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb3in) = 1 Pol(evalfbb4in) = 0 Pol(evalfbb2in) = 1 and size complexities S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-0) = b S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-1) = c S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-2) = d S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-5) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-0) = b S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-1) = c S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-2) = d S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-5) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-0) = b S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-1) = c S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-2) = d S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-3) = 7*a + 7*b + 98 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-5) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-0) = b S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-1) = c S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-2) = d S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-3) = 7*a + 7*b + 98 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-5) = 13*a + 13*b + 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 100 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-5) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-0) = b S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-1) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-2) = d S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-3) = 7*a + 7*b + 98 S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-4) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-5) = ? S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-0) = b S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-1) = c S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-2) = d S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-3) = a S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-4) = e S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-5) = f S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f orients the transitions evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) weakly and the transition evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] strictly and produces the following problem: 10: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (?, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 8*c + 6*a + 6*b + 2, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb3in) = 2*V_4 + 2*V_5 - 2*V_6 + 1 Pol(evalfbb2in) = 2*V_4 + 2*V_5 - 2*V_6 and size complexities S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-0) = b S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-1) = c S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-2) = d S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f)", 0-5) = ? S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-0) = b S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-1) = c S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-2) = d S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-3) = 7*a + 7*b + 98 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f)", 0-5) = ? S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-0) = b S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-1) = c S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-2) = d S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-3) = 7*a + 7*b + 98 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1)", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ]", 0-5) = ? S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-0) = b S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-1) = c S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-2) = d S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-3) = 7*a + 7*b + 98 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ]", 0-5) = ? S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-0) = b S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-1) = c S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-2) = d S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-3) = 7*a + 7*b + 98 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e)", 0-5) = 13*a + 13*b + 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 100 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ]", 0-5) = ? S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-0) = b S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-1) = c S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-2) = d S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-3) = 7*a + 7*b + 98 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-4) = 9*c + 24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 6*a + 6*b + 2 S("evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ]", 0-5) = ? S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-0) = b S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-1) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-2) = d S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-3) = 7*a + 7*b + 98 S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-4) = c S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ]", 0-5) = ? S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-0) = b S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-1) = c S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-2) = d S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-3) = a S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-4) = e S("evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f)", 0-5) = f S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f orients the transitions evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) weakly and the transition evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] strictly and produces the following problem: 11: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (912*a^2*d + 1824*a*b*d + 912*a^2*c + 1824*a*b*c + 5212*a*d + 5224*a*c + 156*a^2 + 312*a*b + 912*b^2*d + 912*b^2*c + 5212*b*d + 5224*b*c + 156*b^2 + 1584*a*c*d + 1584*b*c*d + 816*a*c^2 + 816*b*c^2 + 272*c*d + 144*c^2 + 1152*a^2*d^2 + 2304*a*b*d^2 + 2304*a^2*c*d + 4608*a*b*c*d + 768*a*d^2 + 1152*b^2*d^2 + 2304*b^2*c*d + 768*b*d^2 + 1152*a^2*c^2 + 2304*a*b*c^2 + 1152*b^2*c^2 + 128*d^2 + 1255*a + 1255*b + 1640*c + 1636*d + 401, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (?, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 8*c + 6*a + 6*b + 2, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 Repeatedly propagating knowledge in problem 11 produces the following problem: 12: T: (1, 1) evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f) (1, 1) evalfentryin(a, b, c, d, e, f) -> evalfbb7in(b, c, d, a, e, f) (3*a + 3*b + 1, 1) evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, b, f) [ a >= d ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ c >= e ] (3*a + 3*b + 1, 1) evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e, f) [ e >= c + 1 ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb1in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, d - e) (912*a^2*d + 1824*a*b*d + 912*a^2*c + 1824*a*b*c + 5212*a*d + 5224*a*c + 156*a^2 + 312*a*b + 912*b^2*d + 912*b^2*c + 5212*b*d + 5224*b*c + 156*b^2 + 1584*a*c*d + 1584*b*c*d + 816*a*c^2 + 816*b*c^2 + 272*c*d + 144*c^2 + 1152*a^2*d^2 + 2304*a*b*d^2 + 2304*a^2*c*d + 4608*a*b*c*d + 768*a*d^2 + 1152*b^2*d^2 + 2304*b^2*c*d + 768*b*d^2 + 1152*a^2*c^2 + 2304*a*b*c^2 + 1152*b^2*c^2 + 128*d^2 + 1255*a + 1255*b + 1640*c + 1636*d + 401, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c, d, e, f) [ d + e >= f ] (12*a*d + 12*b*d + 12*a*c + 12*b*c + 4*d + 4*c + 3*a + 3*b + 1, 1) evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ f >= d + e + 1 ] (912*a^2*d + 1824*a*b*d + 912*a^2*c + 1824*a*b*c + 5212*a*d + 5224*a*c + 156*a^2 + 312*a*b + 912*b^2*d + 912*b^2*c + 5212*b*d + 5224*b*c + 156*b^2 + 1584*a*c*d + 1584*b*c*d + 816*a*c^2 + 816*b*c^2 + 272*c*d + 144*c^2 + 1152*a^2*d^2 + 2304*a*b*d^2 + 2304*a^2*c*d + 4608*a*b*c*d + 768*a*d^2 + 1152*b^2*d^2 + 2304*b^2*c*d + 768*b*d^2 + 1152*a^2*c^2 + 2304*a*b*c^2 + 1152*b^2*c^2 + 128*d^2 + 1255*a + 1255*b + 1640*c + 1636*d + 401, 1) evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f + 1) (24*a*d + 24*b*d + 24*a*c + 24*b*c + 8*d + 8*c + 6*a + 6*b + 2, 1) evalfbb4in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e + 1, f) (6*a + 6*b + 2, 1) evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d + 1, e, f) start location: evalfstart leaf cost: 2 Complexity upper bound 2537*a + 2537*b + 10484*a*d + 10484*b*d + 10508*a*c + 10508*b*c + 3292*d + 3300*c + 1824*a^2*d + 3648*a*b*d + 1824*a^2*c + 3648*a*b*c + 312*a^2 + 624*a*b + 1824*b^2*d + 1824*b^2*c + 312*b^2 + 3168*a*c*d + 3168*b*c*d + 1632*a*c^2 + 1632*b*c^2 + 544*c*d + 288*c^2 + 2304*a^2*d^2 + 4608*a*b*d^2 + 4608*a^2*c*d + 9216*a*b*c*d + 1536*a*d^2 + 2304*b^2*d^2 + 4608*b^2*c*d + 1536*b*d^2 + 2304*a^2*c^2 + 4608*a*b*c^2 + 2304*b^2*c^2 + 256*d^2 + 815 Time: 0.510 sec (SMT: 0.463 sec)