YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [B >= C] (?,1) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [B >= E && E >= 1 + C] (?,1) 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [C >= 1 + E && B >= E] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [B >= E && C = E] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [F >= 1 + G] (?,1) 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [0 >= 1 + G && F >= H] (?,1) 7. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [G >= 1 && F >= H] (?,1) 8. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= 1 + J] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [F >= H && G = 0] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [F >= H] (?,1) 11. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= J] (?,1) 12. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [F >= G] (?,1) 13. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [G >= 1 + H] (?,1) 14. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [G >= 0] (?,1) 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [F >= H] (?,1) 16. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 17. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [0 >= 1 + G] (?,1) 18. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= G] (?,1) 19. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [G >= 1 + F] (?,1) 20. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= 1 + G] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 22. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= G] (?,1) 23. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [H >= 1 + F] (?,1) 24. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= F] (?,1) 25. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 1 + B] (?,1) 26. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 1 + B] (?,1) Signature: {(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1,26},1->{2,3,4,25},2->{2,3,4,25},3->{2,3,4,25},4->{2,3,4,25},5->{6,7,9,23},6->{8,22},7->{8,22},8->{8 ,22},9->{6,7,9,23},10->{11,20},11->{11,20},12->{13,18},13->{13,18},14->{15,16},15->{15,16},16->{14,17} ,17->{},18->{12,19},19->{14,17},20->{10,21},21->{5,24},22->{6,7,9,23},23->{10,21},24->{12,19},25->{1,26} ,26->{5,24}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [B >= C] (?,1) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [B >= E && E >= 1 + C] (?,1) 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [C >= 1 + E && B >= E] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [B >= E && C = E] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [F >= 1 + G] (?,1) 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [0 >= 1 + G && F >= H] (?,1) 7. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [G >= 1 && F >= H] (?,1) 8. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= 1 + J] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [F >= H && G = 0] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [F >= H] (?,1) 11. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= J] (?,1) 12. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [F >= G] (?,1) 13. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [G >= 1 + H] (?,1) 14. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [G >= 0] (?,1) 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [F >= H] (?,1) 16. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 17. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [0 >= 1 + G] (1,1) 18. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= G] (?,1) 19. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [G >= 1 + F] (1,1) 20. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= 1 + G] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 22. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= G] (?,1) 23. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [H >= 1 + F] (?,1) 24. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= F] (1,1) 25. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 1 + B] (?,1) 26. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 1 + B] (1,1) Signature: {(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1,26},1->{2,3,4,25},2->{2,3,4,25},3->{2,3,4,25},4->{2,3,4,25},5->{6,7,9,23},6->{8,22},7->{8,22},8->{8 ,22},9->{6,7,9,23},10->{11,20},11->{11,20},12->{13,18},13->{13,18},14->{15,16},15->{15,16},16->{14,17} ,17->{},18->{12,19},19->{14,17},20->{10,21},21->{5,24},22->{6,7,9,23},23->{10,21},24->{12,19},25->{1,26} ,26->{5,24}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,26) ,(2,3) ,(2,4) ,(3,2) ,(4,3) ,(4,4) ,(5,23) ,(6,8) ,(7,22) ,(9,6) ,(9,7)] * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [B >= C] (?,1) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [B >= E && E >= 1 + C] (?,1) 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [C >= 1 + E && B >= E] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [B >= E && C = E] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [F >= 1 + G] (?,1) 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [0 >= 1 + G && F >= H] (?,1) 7. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [G >= 1 && F >= H] (?,1) 8. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= 1 + J] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [F >= H && G = 0] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [F >= H] (?,1) 11. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= J] (?,1) 12. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [F >= G] (?,1) 13. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [G >= 1 + H] (?,1) 14. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [G >= 0] (?,1) 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [F >= H] (?,1) 16. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 17. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [0 >= 1 + G] (1,1) 18. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= G] (?,1) 19. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [G >= 1 + F] (1,1) 20. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= 1 + G] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 22. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= G] (?,1) 23. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [H >= 1 + F] (?,1) 24. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= F] (1,1) 25. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 1 + B] (?,1) 26. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 1 + B] (1,1) Signature: {(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1},1->{2,3,4,25},2->{2,25},3->{3,4,25},4->{2,25},5->{6,7,9},6->{22},7->{8},8->{8,22},9->{9,23} ,10->{11,20},11->{11,20},12->{13,18},13->{13,18},14->{15,16},15->{15,16},16->{14,17},17->{},18->{12,19} ,19->{14,17},20->{10,21},21->{5,24},22->{6,7,9,23},23->{10,21},24->{12,19},25->{1,26},26->{5,24}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [B >= C] (?,1) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [B >= E && E >= 1 + C] (?,1) 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [C >= 1 + E && B >= E] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [B >= E && C = E] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [F >= 1 + G] (?,1) 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [0 >= 1 + G && F >= H] (?,1) 7. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [G >= 1 && F >= H] (?,1) 8. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= 1 + J] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [F >= H && G = 0] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [F >= H] (?,1) 11. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= J] (?,1) 12. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [F >= G] (?,1) 13. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [G >= 1 + H] (?,1) 14. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [G >= 0] (?,1) 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [F >= H] (?,1) 16. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 17. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [0 >= 1 + G] (?,1) 18. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= G] (?,1) 19. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [G >= 1 + F] (?,1) 20. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= 1 + G] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 22. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= G] (?,1) 23. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [H >= 1 + F] (?,1) 24. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= F] (?,1) 25. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 1 + B] (?,1) 26. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 1 + B] (?,1) 27. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) Signature: {(exitus616,13) ;(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1,26},1->{2,3,4,25},2->{2,3,4,25},3->{2,3,4,25},4->{2,3,4,25},5->{6,7,9,23},6->{8,22},7->{8,22},8->{8 ,22},9->{6,7,9,23},10->{11,20},11->{11,20},12->{13,18},13->{13,18},14->{15,16},15->{15,16},16->{14,17,27} ,17->{},18->{12,19},19->{14,17,27},20->{10,21},21->{5,24},22->{6,7,9,23},23->{10,21},24->{12,19},25->{1,26} ,26->{5,24},27->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,26) ,(2,3) ,(2,4) ,(3,2) ,(4,3) ,(4,4) ,(5,23) ,(6,8) ,(7,22) ,(9,6) ,(9,7)] * Step 5: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [B >= C] (?,1) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [B >= E && E >= 1 + C] (?,1) 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [C >= 1 + E && B >= E] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [B >= E && C = E] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [F >= 1 + G] (?,1) 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [0 >= 1 + G && F >= H] (?,1) 7. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [G >= 1 && F >= H] (?,1) 8. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= 1 + J] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [F >= H && G = 0] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [F >= H] (?,1) 11. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= J] (?,1) 12. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [F >= G] (?,1) 13. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [G >= 1 + H] (?,1) 14. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [G >= 0] (?,1) 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [F >= H] (?,1) 16. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 17. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [0 >= 1 + G] (?,1) 18. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= G] (?,1) 19. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [G >= 1 + F] (?,1) 20. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= 1 + G] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 22. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= G] (?,1) 23. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [H >= 1 + F] (?,1) 24. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= F] (?,1) 25. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 1 + B] (?,1) 26. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 1 + B] (?,1) 27. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) Signature: {(exitus616,13) ;(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1},1->{2,3,4,25},2->{2,25},3->{3,4,25},4->{2,25},5->{6,7,9},6->{22},7->{8},8->{8,22},9->{9,23} ,10->{11,20},11->{11,20},12->{13,18},13->{13,18},14->{15,16},15->{15,16},16->{14,17,27},17->{},18->{12,19} ,19->{14,17,27},20->{10,21},21->{5,24},22->{6,7,9,23},23->{10,21},24->{12,19},25->{1,26},26->{5,24},27->{}] + Applied Processor: LooptreeTransformer + 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,23,24,25,26,27] | +- p:[1,25,2,4,3] c: [1] | | | +- p:[3] c: [3] | | | `- p:[2] c: [2] | +- p:[5,21,20,10,23,9,22,6,8,7,11] c: [5] | | | +- p:[6,22,8,7] c: [7] | | | | | +- p:[8] c: [8] | | | | | `- p:[6,22] c: [6] | | | +- p:[9] c: [9] | | | `- p:[10,20,11] c: [10] | | | `- p:[11] c: [11] | +- p:[12,18,13] c: [12] | | | `- p:[13] c: [13] | `- p:[14,16,15] c: [14] | `- p:[15] c: [15] * Step 6: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [B >= C] (?,1) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [B >= E && E >= 1 + C] (?,1) 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [C >= 1 + E && B >= E] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [B >= E && C = E] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [F >= 1 + G] (?,1) 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [0 >= 1 + G && F >= H] (?,1) 7. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [G >= 1 && F >= H] (?,1) 8. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= 1 + J] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [F >= H && G = 0] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [F >= H] (?,1) 11. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [G >= J] (?,1) 12. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [F >= G] (?,1) 13. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [G >= 1 + H] (?,1) 14. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [G >= 0] (?,1) 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [F >= H] (?,1) 16. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 17. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [0 >= 1 + G] (?,1) 18. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= G] (?,1) 19. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [G >= 1 + F] (?,1) 20. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= 1 + G] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 1 + F] (?,1) 22. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [J >= G] (?,1) 23. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [H >= 1 + F] (?,1) 24. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= F] (?,1) 25. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 1 + B] (?,1) 26. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 1 + B] (?,1) 27. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) Signature: {(exitus616,13) ;(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1},1->{2,3,4,25},2->{2,25},3->{3,4,25},4->{2,25},5->{6,7,9},6->{22},7->{8},8->{8,22},9->{9,23} ,10->{11,20},11->{11,20},12->{13,18},13->{13,18},14->{15,16},15->{15,16},16->{14,17,27},17->{},18->{12,19} ,19->{14,17,27},20->{10,21},21->{5,24},22->{6,7,9,23},23->{10,21},24->{12,19},25->{1,26},26->{5,24},27->{}] ,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,23,24,25,26,27] | +- p:[1,25,2,4,3] c: [1] | | | +- p:[3] c: [3] | | | `- p:[2] c: [2] | +- p:[5,21,20,10,23,9,22,6,8,7,11] c: [5] | | | +- p:[6,22,8,7] c: [7] | | | | | +- p:[8] c: [8] | | | | | `- p:[6,22] c: [6] | | | +- p:[9] c: [9] | | | `- p:[10,20,11] c: [10] | | | `- p:[11] c: [11] | +- p:[12,18,13] c: [12] | | | `- p:[13] c: [13] | `- p:[14,16,15] c: [14] | `- p:[15] c: [15]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A ,B ,C ,D ,E ,F ,G ,H ,I ,J ,K ,L ,M ,0.0 ,0.0.0 ,0.0.1 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.1 ,0.1.1 ,0.1.2 ,0.1.2.0 ,0.2 ,0.2.0 ,0.3 ,0.3.0] f0 ~> f15 [A <= 50*K, B <= 5*K, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f15 ~> f19 [A <= A, B <= B, C <= C, D <= 0*K, E <= 0*K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f33 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= F + G, I <= I, J <= J, K <= K, L <= L, M <= M] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f41 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= G + J, K <= K, L <= L, M <= M] f36 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= K + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] f50 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f54 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= K + J, K <= K, L <= L, M <= M] f66 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= unknown, J <= J, K <= K, L <= L, M <= M] f70 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= G + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] f80 ~> f84 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + G, I <= unknown, J <= J, K <= K, L <= L, M <= M] f84 ~> f84 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] f84 ~> f80 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f80 ~> f96 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 0*K, L <= 0*K, M <= M] f70 ~> f66 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f66 ~> f80 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + F, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f54 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] f50 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f41 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] f36 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + G, I <= I, J <= J, K <= K, L <= L, M <= M] f33 ~> f66 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f15 [A <= A, B <= B, C <= K + C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f15 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= B, G <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, M <= A] f80 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] + Loop: [0.0 <= 2*K + B + C] f15 ~> f19 [A <= A, B <= B, C <= C, D <= 0*K, E <= 0*K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f15 [A <= A, B <= B, C <= K + C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] + Loop: [0.0.0 <= K + B + E] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] + Loop: [0.0.1 <= K + B + E] f19 ~> f19 [A <= A, B <= B, C <= C, D <= unknown, E <= K + E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] + Loop: [0.1 <= 2*K + F + G] f33 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= F + G, I <= I, J <= J, K <= K, L <= L, M <= M] f50 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f54 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] f50 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f36 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + G, I <= I, J <= J, K <= K, L <= L, M <= M] f36 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= K + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] f41 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f41 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= G + J, K <= K, L <= L, M <= M] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f54 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= K + J, K <= K, L <= L, M <= M] + Loop: [0.1.0 <= 2*K + F + H] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f41 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] f41 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= G + J, K <= K, L <= L, M <= M] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] + Loop: [0.1.0.0 <= G + J] f41 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= G + J, K <= K, L <= L, M <= M] + Loop: [0.1.0.1 <= 2*K + F + H] f36 ~> f41 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f41 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] + Loop: [0.1.1 <= K + F + H] f36 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= K + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] + Loop: [0.1.2 <= 2*K + F + H] f50 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= 0*K, K <= K, L <= L, M <= M] f54 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= I, J <= J, K <= K, L <= L, M <= M] f54 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= K + J, K <= K, L <= L, M <= M] + Loop: [0.1.2.0 <= K + G + J] f54 ~> f54 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= K + J, K <= K, L <= L, M <= M] + Loop: [0.2 <= 2*K + F + G] f66 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= unknown, J <= J, K <= K, L <= L, M <= M] f70 ~> f66 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f70 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= G + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] + Loop: [0.2.0 <= G + H] f70 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= G + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] + Loop: [0.3 <= 2*K + G] f80 ~> f84 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + G, I <= unknown, J <= J, K <= K, L <= L, M <= M] f84 ~> f80 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M] f84 ~> f84 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] + Loop: [0.3.0 <= K + F + H] f84 ~> f84 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= unknown, J <= J, K <= K, L <= L, M <= M] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick ,huge ,K ,A ,B ,C ,D ,E ,F ,G ,H ,I ,J ,K ,L ,M ,0.0 ,0.0.0 ,0.0.1 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.1 ,0.1.1 ,0.1.2 ,0.1.2.0 ,0.2 ,0.2.0 ,0.3 ,0.3.0] f0 ~> f15 [K ~=> A,K ~=> B,K ~=> C] f15 ~> f19 [K ~=> D,K ~=> E] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] f33 ~> f36 [F ~+> H,G ~+> H] f36 ~> f41 [K ~=> J,huge ~=> I] f36 ~> f41 [K ~=> J,huge ~=> I] f41 ~> f41 [huge ~=> I,G ~+> J,J ~+> J] f36 ~> f36 [K ~=> G,huge ~=> I,H ~+> H,K ~+> H] f50 ~> f54 [K ~=> J,huge ~=> I] f54 ~> f54 [huge ~=> I,J ~+> J,K ~+> J] f66 ~> f70 [K ~=> H,huge ~=> I] f70 ~> f70 [huge ~=> I,G ~+> H,H ~+> H] f80 ~> f84 [huge ~=> I,G ~+> H,K ~+> H] f84 ~> f84 [huge ~=> I,H ~+> H,K ~+> H] f84 ~> f80 [G ~+> G,K ~+> G] f80 ~> f96 [K ~=> K,K ~=> L] f70 ~> f66 [G ~+> G,K ~+> G] f66 ~> f80 [F ~+> G,K ~+> G] f54 ~> f50 [H ~+> H,K ~+> H] f50 ~> f33 [G ~+> G,K ~+> G] f41 ~> f36 [H ~+> H,K ~+> H] f36 ~> f50 [G ~+> H,K ~+> H] f33 ~> f66 [K ~=> G] f19 ~> f15 [C ~+> C,K ~+> C] f15 ~> f33 [A ~=> M,B ~=> F,K ~=> G] f80 ~> exitus616 [] + Loop: [B ~+> 0.0,C ~+> 0.0,K ~*> 0.0] f15 ~> f19 [K ~=> D,K ~=> E] f19 ~> f15 [C ~+> C,K ~+> C] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] + Loop: [B ~+> 0.0.0,E ~+> 0.0.0,K ~+> 0.0.0] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] + Loop: [B ~+> 0.0.1,E ~+> 0.0.1,K ~+> 0.0.1] f19 ~> f19 [huge ~=> D,E ~+> E,K ~+> E] + Loop: [F ~+> 0.1,G ~+> 0.1,K ~*> 0.1] f33 ~> f36 [F ~+> H,G ~+> H] f50 ~> f33 [G ~+> G,K ~+> G] f54 ~> f50 [H ~+> H,K ~+> H] f50 ~> f54 [K ~=> J,huge ~=> I] f36 ~> f50 [G ~+> H,K ~+> H] f36 ~> f36 [K ~=> G,huge ~=> I,H ~+> H,K ~+> H] f41 ~> f36 [H ~+> H,K ~+> H] f36 ~> f41 [K ~=> J,huge ~=> I] f41 ~> f41 [huge ~=> I,G ~+> J,J ~+> J] f36 ~> f41 [K ~=> J,huge ~=> I] f54 ~> f54 [huge ~=> I,J ~+> J,K ~+> J] + Loop: [F ~+> 0.1.0,H ~+> 0.1.0,K ~*> 0.1.0] f36 ~> f41 [K ~=> J,huge ~=> I] f41 ~> f36 [H ~+> H,K ~+> H] f41 ~> f41 [huge ~=> I,G ~+> J,J ~+> J] f36 ~> f41 [K ~=> J,huge ~=> I] + Loop: [G ~+> 0.1.0.0,J ~+> 0.1.0.0] f41 ~> f41 [huge ~=> I,G ~+> J,J ~+> J] + Loop: [F ~+> 0.1.0.1,H ~+> 0.1.0.1,K ~*> 0.1.0.1] f36 ~> f41 [K ~=> J,huge ~=> I] f41 ~> f36 [H ~+> H,K ~+> H] + Loop: [F ~+> 0.1.1,H ~+> 0.1.1,K ~+> 0.1.1] f36 ~> f36 [K ~=> G,huge ~=> I,H ~+> H,K ~+> H] + Loop: [F ~+> 0.1.2,H ~+> 0.1.2,K ~*> 0.1.2] f50 ~> f54 [K ~=> J,huge ~=> I] f54 ~> f50 [H ~+> H,K ~+> H] f54 ~> f54 [huge ~=> I,J ~+> J,K ~+> J] + Loop: [G ~+> 0.1.2.0,J ~+> 0.1.2.0,K ~+> 0.1.2.0] f54 ~> f54 [huge ~=> I,J ~+> J,K ~+> J] + Loop: [F ~+> 0.2,G ~+> 0.2,K ~*> 0.2] f66 ~> f70 [K ~=> H,huge ~=> I] f70 ~> f66 [G ~+> G,K ~+> G] f70 ~> f70 [huge ~=> I,G ~+> H,H ~+> H] + Loop: [G ~+> 0.2.0,H ~+> 0.2.0] f70 ~> f70 [huge ~=> I,G ~+> H,H ~+> H] + Loop: [G ~+> 0.3,K ~*> 0.3] f80 ~> f84 [huge ~=> I,G ~+> H,K ~+> H] f84 ~> f80 [G ~+> G,K ~+> G] f84 ~> f84 [huge ~=> I,H ~+> H,K ~+> H] + Loop: [F ~+> 0.3.0,H ~+> 0.3.0,K ~+> 0.3.0] f84 ~> f84 [huge ~=> I,H ~+> H,K ~+> H] + Applied Processor: LareProcessor + Details: f0 ~> f96 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,K ~=> F ,K ~=> H ,K ~=> J ,K ~=> K ,K ~=> L ,K ~=> M ,huge ~=> D ,huge ~=> I ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> E ,K ~+> G ,K ~+> H ,K ~+> J ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.1 ,K ~+> 0.1.2 ,K ~+> 0.1.2.0 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.3 ,K ~+> 0.3.0 ,K ~+> tick ,J ~*> J ,J ~*> 0.1.0.0 ,J ~*> tick ,K ~*> C ,K ~*> E ,K ~*> G ,K ~*> H ,K ~*> J ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.1 ,K ~*> 0.1.2 ,K ~*> 0.1.2.0 ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> tick ,K ~^> E ,K ~^> H ,K ~^> J ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.1 ,K ~^> tick] f0 ~> exitus616 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,K ~=> F ,K ~=> H ,K ~=> J ,K ~=> M ,huge ~=> D ,huge ~=> I ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> E ,K ~+> G ,K ~+> H ,K ~+> J ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.1 ,K ~+> 0.1.2 ,K ~+> 0.1.2.0 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.3 ,K ~+> 0.3.0 ,K ~+> tick ,J ~*> J ,J ~*> 0.1.0.0 ,J ~*> tick ,K ~*> C ,K ~*> E ,K ~*> G ,K ~*> H ,K ~*> J ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.1 ,K ~*> 0.1.2 ,K ~*> 0.1.2.0 ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> tick ,K ~^> E ,K ~^> H ,K ~^> J ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.1 ,K ~^> tick] + f15> [K ~=> D ,K ~=> E ,huge ~=> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,C ~+> C ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> E ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,B ~*> C ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,C ~*> C ,C ~*> E ,C ~*> tick ,K ~*> C ,K ~*> E ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,B ~^> E ,C ~^> E ,K ~^> E] + f19> [huge ~=> D ,B ~+> 0.0.0 ,B ~+> tick ,E ~+> E ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> E ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> E ,E ~*> E ,K ~*> E] + f19> [huge ~=> D ,B ~+> 0.0.1 ,B ~+> tick ,E ~+> E ,E ~+> 0.0.1 ,E ~+> tick ,tick ~+> tick ,K ~+> E ,K ~+> 0.0.1 ,K ~+> tick ,B ~*> E ,E ~*> E ,K ~*> E] + f33> [K ~=> G ,K ~=> J ,huge ~=> I ,F ~+> H ,F ~+> 0.1 ,F ~+> 0.1.0 ,F ~+> 0.1.0.1 ,F ~+> 0.1.1 ,F ~+> 0.1.2 ,F ~+> tick ,G ~+> G ,G ~+> H ,G ~+> J ,G ~+> 0.1 ,G ~+> 0.1.0 ,G ~+> 0.1.0.0 ,G ~+> 0.1.0.1 ,G ~+> 0.1.1 ,G ~+> 0.1.2 ,G ~+> 0.1.2.0 ,G ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> G ,K ~+> H ,K ~+> J ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.1 ,K ~+> 0.1.2 ,K ~+> 0.1.2.0 ,K ~+> tick ,F ~*> G ,F ~*> H ,F ~*> J ,F ~*> 0.1.0 ,F ~*> 0.1.0.0 ,F ~*> 0.1.0.1 ,F ~*> 0.1.1 ,F ~*> 0.1.2 ,F ~*> 0.1.2.0 ,F ~*> tick ,G ~*> G ,G ~*> H ,G ~*> J ,G ~*> 0.1.0 ,G ~*> 0.1.0.0 ,G ~*> 0.1.0.1 ,G ~*> 0.1.1 ,G ~*> 0.1.2 ,G ~*> 0.1.2.0 ,G ~*> tick ,J ~*> J ,J ~*> 0.1.0.0 ,J ~*> tick ,K ~*> G ,K ~*> H ,K ~*> J ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.1 ,K ~*> 0.1.2 ,K ~*> 0.1.2.0 ,K ~*> tick ,F ~^> H ,F ~^> J ,F ~^> 0.1.0 ,F ~^> 0.1.0.0 ,F ~^> 0.1.0.1 ,F ~^> 0.1.1 ,F ~^> tick ,G ~^> H ,G ~^> J ,G ~^> 0.1.0 ,G ~^> 0.1.0.0 ,G ~^> 0.1.0.1 ,G ~^> 0.1.1 ,G ~^> tick ,K ~^> H ,K ~^> J ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.1 ,K ~^> tick] + f36> [K ~=> J ,huge ~=> I ,F ~+> 0.1.0 ,F ~+> 0.1.0.1 ,F ~+> tick ,G ~+> J ,G ~+> 0.1.0.0 ,G ~+> tick ,H ~+> H ,H ~+> 0.1.0 ,H ~+> 0.1.0.1 ,H ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> J ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.1 ,K ~+> tick ,F ~*> H ,F ~*> J ,F ~*> 0.1.0.0 ,F ~*> 0.1.0.1 ,F ~*> tick ,G ~*> J ,G ~*> 0.1.0.0 ,G ~*> tick ,H ~*> H ,H ~*> J ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.1 ,H ~*> tick ,J ~*> J ,J ~*> 0.1.0.0 ,J ~*> tick ,K ~*> H ,K ~*> J ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.1 ,K ~*> tick ,F ~^> H ,F ~^> J ,F ~^> 0.1.0.0 ,F ~^> 0.1.0.1 ,F ~^> tick ,H ~^> H ,H ~^> J ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.1 ,H ~^> tick ,K ~^> H ,K ~^> J ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.1 ,K ~^> tick] + f41> [huge ~=> I ,G ~+> J ,G ~+> 0.1.0.0 ,G ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,tick ~+> tick ,G ~*> J ,J ~*> J] + f41> [K ~=> J ,huge ~=> I ,F ~+> 0.1.0.1 ,F ~+> tick ,H ~+> H ,H ~+> 0.1.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,F ~*> H ,H ~*> H ,K ~*> H ,K ~*> 0.1.0.1 ,K ~*> tick] f36> [K ~=> J ,huge ~=> I ,F ~+> 0.1.0.1 ,F ~+> tick ,H ~+> H ,H ~+> 0.1.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,F ~*> H ,H ~*> H ,K ~*> H ,K ~*> 0.1.0.1 ,K ~*> tick] f41> [K ~=> J ,huge ~=> I ,F ~+> 0.1.0.1 ,F ~+> tick ,H ~+> H ,H ~+> 0.1.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,F ~*> H ,H ~*> H ,K ~*> H ,K ~*> 0.1.0.1 ,K ~*> tick] f36> [K ~=> J ,huge ~=> I ,F ~+> 0.1.0.1 ,F ~+> tick ,H ~+> H ,H ~+> 0.1.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,F ~*> H ,H ~*> H ,K ~*> H ,K ~*> 0.1.0.1 ,K ~*> tick] + f36> [K ~=> G ,huge ~=> I ,F ~+> 0.1.1 ,F ~+> tick ,H ~+> H ,H ~+> 0.1.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1.1 ,K ~+> tick ,F ~*> H ,H ~*> H ,K ~*> H] + f50> [K ~=> J ,huge ~=> I ,F ~+> 0.1.2 ,F ~+> tick ,G ~+> 0.1.2.0 ,G ~+> tick ,H ~+> H ,H ~+> 0.1.2 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> J ,K ~+> 0.1.2.0 ,K ~+> tick ,F ~*> H ,F ~*> J ,F ~*> tick ,G ~*> J ,G ~*> 0.1.2.0 ,G ~*> tick ,H ~*> H ,H ~*> J ,H ~*> tick ,K ~*> H ,K ~*> J ,K ~*> 0.1.2 ,K ~*> 0.1.2.0 ,K ~*> tick ,F ~^> J ,H ~^> J ,K ~^> J] + f54> [huge ~=> I ,G ~+> 0.1.2.0 ,G ~+> tick ,J ~+> J ,J ~+> 0.1.2.0 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,K ~+> 0.1.2.0 ,K ~+> tick ,G ~*> J ,J ~*> J ,K ~*> J] + f66> [K ~=> H ,huge ~=> I ,F ~+> 0.2 ,F ~+> tick ,G ~+> G ,G ~+> H ,G ~+> 0.2 ,G ~+> 0.2.0 ,G ~+> tick ,tick ~+> tick ,K ~+> G ,K ~+> H ,K ~+> 0.2.0 ,K ~+> tick ,F ~*> G ,F ~*> H ,F ~*> tick ,G ~*> G ,G ~*> H ,G ~*> 0.2.0 ,G ~*> tick ,K ~*> G ,K ~*> H ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> tick ,F ~^> H ,G ~^> H ,K ~^> H] + f70> [huge ~=> I ,G ~+> H ,G ~+> 0.2.0 ,G ~+> tick ,H ~+> H ,H ~+> 0.2.0 ,H ~+> tick ,tick ~+> tick ,G ~*> H ,H ~*> H] + f80> [huge ~=> I ,F ~+> 0.3.0 ,F ~+> tick ,G ~+> G ,G ~+> H ,G ~+> 0.3 ,G ~+> 0.3.0 ,G ~+> tick ,tick ~+> tick ,K ~+> G ,K ~+> H ,K ~+> 0.3.0 ,K ~+> tick ,F ~*> H ,F ~*> 0.3.0 ,F ~*> tick ,G ~*> G ,G ~*> H ,G ~*> 0.3.0 ,G ~*> tick ,K ~*> G ,K ~*> H ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> tick ,G ~^> H ,K ~^> H] + f84> [huge ~=> I ,F ~+> 0.3.0 ,F ~+> tick ,H ~+> H ,H ~+> 0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.3.0 ,K ~+> tick ,F ~*> H ,H ~*> H ,K ~*> H] YES(?,POLY)