YES(?,POLY) * Step 1: ArgumentFilter WORST_CASE(?,POLY) + 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: ArgumentFilter [4,5,6,8,9] + Details: We remove following argument positions: [4,5,6,8,9]. * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,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,H,K) -> f71(A,B,C,D,H,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,H,K) -> f5(A,B,C,D,H,K) True (1,1) 3. f5(A,B,C,D,H,K) -> f9(A,B,0,D,H,K) [A >= B] (?,1) 4. f9(A,B,C,D,H,K) -> f9(A,B,C,1 + D,H,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,H,K) -> f9(A,B,L,1 + D,H,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,H,K) -> f26(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,H,K) -> f59(A,B,C,D,1 + H,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,H,K) -> f71(A,B,C,D,H,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,H,K) -> f74(A,B,C,D,H,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,H,K) -> f23(A,B,C,1 + A,H,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,H,K) -> f23(A,B,C,1 + D,H,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,H,K) -> f69(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f69(A,B,C,D,H,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,H,K) -> f40(A,B,0,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,H,K) -> f1(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 18. f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 20. f9(A,B,C,D,H,K) -> f5(A,1 + B,0,D,H,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 21. f5(A,B,C,D,H,K) -> f23(A,B,C,D,H,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 3: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,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,H,K) -> f71(A,B,C,D,H,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,H,K) -> f5(A,B,C,D,H,K) True (1,1) 3. f5(A,B,C,D,H,K) -> f9(A,B,0,D,H,K) [A >= B] (?,1) 4. f9(A,B,C,D,H,K) -> f9(A,B,C,1 + D,H,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f9(A,B,C,D,H,K) -> f9(A,B,L,1 + D,H,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,H,K) -> f26(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,H,K) -> f59(A,B,C,D,1 + H,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,H,K) -> f71(A,B,C,D,H,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,H,K) -> f74(A,B,C,D,H,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,H,K) -> f23(A,B,C,1 + A,H,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,H,K) -> f23(A,B,C,1 + D,H,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,H,K) -> f69(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f69(A,B,C,D,H,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,H,K) -> f40(A,B,0,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 17. f23(A,B,C,D,H,K) -> f1(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 18. f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 20. f9(A,B,C,D,H,K) -> f5(A,1 + B,0,D,H,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 21. f5(A,B,C,D,H,K) -> f23(A,B,C,D,H,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: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,K) [-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,H,K) -> f71(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] f2(A,B,C,D,H,K) -> f5(A,B,C,D,H,K) True f5(A,B,C,D,H,K) -> f9(A,B,0,D,H,K) [A >= B] f9(A,B,C,D,H,K) -> f9(A,B,C,1 + D,H,K) [A + -1*B >= 0 && C >= L && A >= D] f9(A,B,C,D,H,K) -> f9(A,B,L,1 + D,H,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] f23(A,B,C,D,H,K) -> f26(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && A >= D] f59(A,B,C,D,H,K) -> f59(A,B,C,D,1 + H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] f71(A,B,C,D,H,K) -> f74(A,B,C,D,H,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,H,K) -> f23(A,B,C,1 + A,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] f74(A,B,C,D,H,K) -> f23(A,B,C,1 + D,H,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f59(A,B,C,D,H,K) -> f69(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] f40(A,B,C,D,H,K) -> f59(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f69(A,B,C,D,H,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] f26(A,B,C,D,H,K) -> f40(A,B,0,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] f23(A,B,C,D,H,K) -> f1(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,0,D,H,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] f5(A,B,C,D,H,K) -> f23(A,B,C,D,H,K) [B >= 1 + A] Signature: {(f1,11);(f2,11);(f23,11);(f26,11);(f40,11);(f5,11);(f59,11);(f69,11);(f71,11);(f74,11);(f9,11)} Rule 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: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,K) [-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,H,K) -> f71(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] f2(A,B,C,D,H,K) -> f5(A,B,C,D,H,K) True f5(A,B,C,D,H,K) -> f9(A,B,0,D,H,K) [A >= B] f9(A,B,C,D,H,K) -> f9(A,B,C,1 + D,H,K) [A + -1*B >= 0 && C >= L && A >= D] f9(A,B,C,D,H,K) -> f9(A,B,L,1 + D,H,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] f23(A,B,C,D,H,K) -> f26(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && A >= D] f59(A,B,C,D,H,K) -> f59(A,B,C,D,1 + H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] f71(A,B,C,D,H,K) -> f74(A,B,C,D,H,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,H,K) -> f23(A,B,C,1 + A,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] f74(A,B,C,D,H,K) -> f23(A,B,C,1 + D,H,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f59(A,B,C,D,H,K) -> f69(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] f40(A,B,C,D,H,K) -> f59(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f69(A,B,C,D,H,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] f26(A,B,C,D,H,K) -> f40(A,B,0,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] f23(A,B,C,D,H,K) -> f1(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,0,D,H,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] f5(A,B,C,D,H,K) -> f23(A,B,C,D,H,K) [B >= 1 + A] f1(A,B,C,D,H,K) -> exitus616(A,B,C,D,H,K) True Signature: {(exitus616,6) ;(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f40,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Rule 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->{22},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22] | +- p:[3,18,4,5,19,20] c: [3,4,5,18,19,20] | `- p:[0,12,7,13,16,6,11,9,1,15,8,14] c: [0,1,6,7,8,9,11,12,13,14,15,16] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,K) [-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,H,K) -> f71(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && L >= 1] f2(A,B,C,D,H,K) -> f5(A,B,C,D,H,K) True f5(A,B,C,D,H,K) -> f9(A,B,0,D,H,K) [A >= B] f9(A,B,C,D,H,K) -> f9(A,B,C,1 + D,H,K) [A + -1*B >= 0 && C >= L && A >= D] f9(A,B,C,D,H,K) -> f9(A,B,L,1 + D,H,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] f23(A,B,C,D,H,K) -> f26(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && A >= D] f59(A,B,C,D,H,K) -> f59(A,B,C,D,1 + H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] f69(A,B,C,D,H,K) -> f71(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] f71(A,B,C,D,H,K) -> f74(A,B,C,D,H,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,H,K) -> f23(A,B,C,1 + A,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] f74(A,B,C,D,H,K) -> f23(A,B,C,1 + D,H,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f59(A,B,C,D,H,K) -> f69(A,B,C,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] f40(A,B,C,D,H,K) -> f59(A,B,C,D,H,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,H,K) -> f59(A,B,C,D,H,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,H,K) -> f69(A,B,C,D,H,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] f26(A,B,C,D,H,K) -> f40(A,B,0,D,H,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] f23(A,B,C,D,H,K) -> f1(A,B,C,D,H,K) [-1 + -1*A + B >= 0 && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,C,D,H,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] f9(A,B,C,D,H,K) -> f5(A,1 + B,0,D,H,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] f5(A,B,C,D,H,K) -> f23(A,B,C,D,H,K) [B >= 1 + A] f1(A,B,C,D,H,K) -> exitus616(A,B,C,D,H,K) True Signature: {(exitus616,6) ;(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f40,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Rule 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->{22},18->{3,21} ,19->{3,21},20->{3,21},21->{6,17}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22] | +- p:[3,18,4,5,19,20] c: [3,4,5,18,19,20] | `- p:[0,12,7,13,16,6,11,9,1,15,8,14] c: [0,1,6,7,8,9,11,12,13,14,15,16]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,H,K,0.0,0.1] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f2 ~> f5 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f5 ~> f9 [A <= A, B <= B, C <= 0*K, D <= D, H <= H, K <= K] f9 ~> f9 [A <= A, B <= B, C <= C, D <= K + D, H <= H, K <= K] f9 ~> f9 [A <= A, B <= B, C <= unknown, D <= K + D, H <= H, K <= K] f23 ~> f26 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, H <= K + H, K <= K] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f71 ~> f74 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f71 ~> f23 [A <= A, B <= B, C <= C, D <= B + D, H <= H, K <= K] f74 ~> f23 [A <= A, B <= B, C <= C, D <= B + D, H <= H, K <= K] f59 ~> f69 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f40 ~> f69 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= D] f26 ~> f40 [A <= A, B <= B, C <= 0*K, D <= D, H <= H, K <= K] f23 ~> f1 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, H <= H, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, H <= H, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= 0*K, D <= D, H <= H, K <= K] f5 ~> f23 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f1 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] + Loop: [0.0 <= A + B + D] f5 ~> f9 [A <= A, B <= B, C <= 0*K, D <= D, H <= H, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, H <= H, K <= K] f9 ~> f9 [A <= A, B <= B, C <= C, D <= K + D, H <= H, K <= K] f9 ~> f9 [A <= A, B <= B, C <= unknown, D <= K + D, H <= H, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, H <= H, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= 0*K, D <= D, H <= H, K <= K] + Loop: [0.1 <= K + A + D + H] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f59 ~> f69 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, H <= K + H, K <= K] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f26 ~> f40 [A <= A, B <= B, C <= 0*K, D <= D, H <= H, K <= K] f23 ~> f26 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f74 ~> f23 [A <= A, B <= B, C <= C, D <= B + D, H <= H, K <= K] f71 ~> f74 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f40 ~> f69 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= D] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, H <= H, K <= K] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,H,K,0.0,0.1] f69 ~> f71 [] f69 ~> f71 [] f2 ~> f5 [] f5 ~> f9 [K ~=> C] f9 ~> f9 [D ~+> D,K ~+> D] f9 ~> f9 [huge ~=> C,D ~+> D,K ~+> D] f23 ~> f26 [] f59 ~> f59 [H ~+> H,K ~+> H] f69 ~> f71 [] f71 ~> f74 [] f71 ~> f23 [B ~+> D,D ~+> D] f74 ~> f23 [B ~+> D,D ~+> D] f59 ~> f69 [] f40 ~> f59 [] f40 ~> f59 [] f40 ~> f69 [D ~=> K] f26 ~> f40 [K ~=> C] f23 ~> f1 [] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [K ~=> C,B ~+> B,K ~+> B] f5 ~> f23 [] f1 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,D ~+> 0.0] f5 ~> f9 [K ~=> C] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f9 [D ~+> D,K ~+> D] f9 ~> f9 [huge ~=> C,D ~+> D,K ~+> D] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [K ~=> C,B ~+> B,K ~+> B] + Loop: [A ~+> 0.1,D ~+> 0.1,H ~+> 0.1,K ~+> 0.1] f69 ~> f71 [] f59 ~> f69 [] f59 ~> f59 [H ~+> H,K ~+> H] f40 ~> f59 [] f26 ~> f40 [K ~=> C] f23 ~> f26 [] f74 ~> f23 [B ~+> D,D ~+> D] f71 ~> f74 [] f69 ~> f71 [] f40 ~> f69 [D ~=> K] f69 ~> f71 [] f40 ~> f59 [] + Applied Processor: Lare + Details: f2 ~> exitus616 [D ~=> K ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> K ,B ~+> 0.0 ,B ~+> tick ,D ~+> D ,D ~+> K ,D ~+> 0.0 ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.1 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.1 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> H ,B ~*> K ,B ~*> 0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.1 ,D ~*> tick ,H ~*> D ,H ~*> H ,H ~*> K ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.1 ,K ~*> tick] + f5> [K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,A ~*> B ,A ~*> D ,B ~*> B ,B ~*> D ,D ~*> B ,D ~*> D ,K ~*> B ,K ~*> D] + f71> [D ~=> K ,K ~=> C ,A ~+> 0.1 ,A ~+> tick ,B ~+> D ,B ~+> K ,D ~+> D ,D ~+> K ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1 ,K ~+> tick ,A ~*> D ,A ~*> H ,B ~*> D ,B ~*> K ,D ~*> D ,D ~*> H ,H ~*> D ,H ~*> H ,K ~*> D ,K ~*> H] f23> [D ~=> K ,K ~=> C ,A ~+> 0.1 ,A ~+> tick ,B ~+> D ,B ~+> K ,D ~+> D ,D ~+> K ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1 ,K ~+> tick ,A ~*> D ,A ~*> H ,A ~*> K ,B ~*> D ,B ~*> K ,D ~*> D ,D ~*> H ,D ~*> K ,H ~*> D ,H ~*> H ,H ~*> K ,K ~*> D ,K ~*> H ,K ~*> K] YES(?,POLY)