YES(?,O(n^1)) * Step 1: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,18,19,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12} ,8->{9,10},9->{11},10->{6,17},11->{6,17},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{} ,18->{3,21},19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,18),(3,19),(10,6),(11,17)] * Step 2: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x1 + -1*x2 p(f2) = 1 + x1 + -1*x2 p(f23) = x1 + -1*x2 p(f26) = x1 + -1*x2 p(f40) = x1 + -1*x2 p(f5) = 1 + x1 + -1*x2 p(f59) = x1 + -1*x2 p(f69) = x1 + -1*x2 p(f71) = x1 + -1*x2 p(f74) = x1 + -1*x2 p(f9) = 1 + x1 + -1*x2 Following rules are strictly oriented: [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B > A + -1*B = f5(A,1 + B,0,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= A + -1*B = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= A + -1*B = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= A + -1*B = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x1 + -1*x2 p(f2) = 1 + x1 + -1*x2 p(f23) = x1 + -1*x2 p(f26) = x1 + -1*x2 p(f40) = x1 + -1*x2 p(f5) = 1 + x1 + -1*x2 p(f59) = x1 + -1*x2 p(f69) = x1 + -1*x2 p(f71) = x1 + -1*x2 p(f74) = x1 + -1*x2 p(f9) = 1 + x1 + -1*x2 Following rules are strictly oriented: [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B > A + -1*B = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B > A + -1*B = f5(A,1 + B,0,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= A + -1*B = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= A + -1*B = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x1 + -1*x2 p(f2) = 1 + x1 + -1*x2 p(f23) = x1 + -1*x2 p(f26) = x1 + -1*x2 p(f40) = x1 + -1*x2 p(f5) = 1 + x1 + -1*x2 p(f59) = x1 + -1*x2 p(f69) = x1 + -1*x2 p(f71) = x1 + -1*x2 p(f74) = x1 + -1*x2 p(f9) = 1 + x1 + -1*x2 Following rules are strictly oriented: [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B > A + -1*B = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B > A + -1*B = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B > A + -1*B = f5(A,1 + B,0,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= 1 + A + -1*B = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*B >= A + -1*B = f1(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*B >= A + -1*B = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 7: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 1 + x1 + -1*x4 p(f2) = 1 + x1 + -1*x4 p(f23) = 1 + x1 + -1*x4 p(f26) = 1 + x1 + -1*x4 p(f40) = x1 + -1*x4 p(f5) = 1 + x1 + -1*x4 p(f59) = x1 + -1*x4 p(f69) = x1 + -1*x4 p(f71) = x1 + -1*x4 p(f74) = x1 + -1*x4 p(f9) = 1 + x1 + -1*x4 Following rules are strictly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D > A + -1*D = f40(A,B,0,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= 0 = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 8: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 9: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 1 + x1 + -1*x4 p(f2) = 1 + x1 + -1*x4 p(f23) = 1 + x1 + -1*x4 p(f26) = 1 + x1 + -1*x4 p(f40) = 1 + x1 + -1*x4 p(f5) = 1 + x1 + -1*x4 p(f59) = 1 + x1 + -1*x4 p(f69) = 1 + x1 + -1*x4 p(f71) = x1 + -1*x4 p(f74) = x1 + -1*x4 p(f9) = 1 + x1 + -1*x4 Following rules are strictly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D > A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= 0 = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 10: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 2 + x1 + -1*x4 p(f2) = 2 + x1 + -1*x4 p(f23) = 2 + x1 + -1*x4 p(f26) = 2 + x1 + -1*x4 p(f40) = 2 + x1 + -1*x4 p(f5) = 2 + x1 + -1*x4 p(f59) = 2 + x1 + -1*x4 p(f69) = 1 + x1 + -1*x4 p(f71) = 1 + x1 + -1*x4 p(f74) = 1 + x1 + -1*x4 p(f9) = 2 + x1 + -1*x4 Following rules are strictly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D > 1 + A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D > 1 + A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,D) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 1 + A + -1*D = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 1 + A + -1*D = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 2 + A + -1*D >= 2 + A + -1*D = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 11: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 12: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (3 + 2*A + 2*D,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (3 + 2*A + 2*D,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x1 + -1*x4 p(f2) = x1 + -1*x4 p(f23) = x1 + -1*x4 p(f26) = x1 + -1*x4 p(f40) = x1 + -1*x4 p(f5) = x1 + -1*x4 p(f59) = x1 + -1*x4 p(f69) = x1 + -1*x4 p(f71) = x1 + -1*x4 p(f74) = x1 + -1*x4 p(f9) = x1 + -1*x4 Following rules are strictly oriented: [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D > -1 + A + -1*D = f23(A,B,C,1 + D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= -1 + A + -1*D = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= -1 + A + -1*D = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= -1 = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 13: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (3 + 2*A + 2*D,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (3 + 2*A + 2*D,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (A + D,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 14: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (3 + 2*A + 2*D,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (1 + A + D,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (3 + 2*A + 2*D,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (7 + 5*A + 5*D,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (A + D,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 1 + x1 + -1*x8 p(f2) = 1 + x1 + -1*x8 p(f23) = 1 + x1 + -1*x8 p(f26) = 1 + x1 + -1*x8 p(f40) = 1 + x1 + -1*x8 p(f5) = 1 + x1 + -1*x8 p(f59) = 1 + x1 + -1*x8 p(f69) = 1 + x1 + -1*x8 p(f71) = 1 + x1 + -1*x8 p(f74) = 1 + x1 + -1*x8 p(f9) = 1 + x1 + -1*x8 Following rules are strictly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H > A + -1*H = f59(A,B,C,D,E,F,G,1 + H,L,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*H >= 1 + A + -1*H = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 15: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (3 + 2*A + 2*D,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (1 + A + D,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (1 + A + H,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (3 + 2*A + 2*D,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (7 + 5*A + 5*D,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (A + D,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 1 + x1 + -1*x4 p(f2) = 1 + x1 + -1*x4 p(f23) = 1 + x1 + -1*x4 p(f26) = x1 + -1*x4 p(f40) = x1 + -1*x4 p(f5) = 1 + x1 + -1*x4 p(f59) = x1 + -1*x4 p(f69) = x1 + -1*x4 p(f71) = x1 + -1*x4 p(f74) = x1 + -1*x4 p(f9) = 1 + x1 + -1*x4 Following rules are strictly oriented: [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D > A + -1*D = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D > A + -1*D = f26(A,B,C,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f9(A,B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= A + -1*D = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= 0 = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = A + -1*D >= A + -1*D = f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 1 + A + -1*D >= 1 + A + -1*D = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 16: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (3 + 2*A + 2*D,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (1 + A + D,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (1 + A + D,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (1 + A + H,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (3 + 2*A + 2*D,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (7 + 5*A + 5*D,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (A + D,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 2 + 2*x1 + -2*x4 p(f2) = 2 + 2*x1 + -2*x4 p(f23) = 2 + 2*x1 + -2*x4 p(f26) = 1 + 2*x1 + -2*x4 p(f40) = 2*x1 + -2*x4 p(f5) = 2 + 2*x1 + -2*x4 p(f59) = 2*x1 + -2*x4 p(f69) = 2*x1 + -2*x4 p(f71) = 2*x1 + -2*x4 p(f74) = 2*x1 + -2*x4 p(f9) = 2 + 2*x1 + -2*x4 Following rules are strictly oriented: [A + -1*B >= 0 && C >= L && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D > 2*A + -2*D = f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D > 2*A + -2*D = f9(A,B,L,1 + D,L,L,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D > 1 + 2*A + -2*D = f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] ==> f26(A,B,C,D,E,F,G,H,I,J,K) = 1 + 2*A + -2*D > 2*A + -2*D = f40(A,B,0,D,E,F,G,H,I,J,K) Following rules are weakly oriented: [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f71(A,B,C,D,E,F,G,H,I,J,K) True ==> f2(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f5(A,B,C,D,E,F,G,H,I,J,K) [A >= B] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f9(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] ==> f69(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] ==> f71(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 0 = f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] ==> f74(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] ==> f59(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 ==> && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] f40(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] ==> f40(A,B,C,D,E,F,G,H,I,J,K) = 2*A + -2*D >= 2*A + -2*D = f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + -1*A + B >= 0 && D >= 1 + A] ==> f23(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f1(A,B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] ==> f9(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f5(A,1 + B,0,D,E,F,G,H,I,J,K) [B >= 1 + A] ==> f5(A,B,C,D,E,F,G,H,I,J,K) = 2 + 2*A + -2*D >= 2 + 2*A + -2*D = f23(A,B,C,D,E,F,G,H,I,J,K) * Step 17: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (3 + 2*A + 2*D,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] (1 + A + D,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (4 + 3*A + 3*B,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (2 + 2*A + 2*D,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (1 + A + D,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (1 + A + D,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (1 + A + H,1) 8. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (3 + 2*A + 2*D,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (7 + 5*A + 5*D,1) 10. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (1,1) 11. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (A + D,1) 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (2 + A + D,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 14. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (1 + A + D,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 15. f40(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (1 + A + D,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (1 + A + D,1) 17. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (1 + A + B,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (1 + A + B,1) 20. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (1 + A + B,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Flow Graph: [0->{9,10},1->{9,10},2->{3,21},3->{4,5,20},4->{4,5,18,19,20},5->{4,5,18,19,20},6->{16},7->{7,12},8->{9,10} ,9->{11},10->{17},11->{6},12->{0,1,8},13->{7,12},14->{7,12},15->{0,1,8},16->{13,14,15},17->{},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))