YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalperfectstart(A,B,C,D) -> evalperfectentryin(A,B,C,D) True (1,1) 1. evalperfectentryin(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [1 >= A] (?,1) 2. evalperfectentryin(A,B,C,D) -> evalperfectbb1in(A,B,C,D) [A >= 2] (?,1) 3. evalperfectbb1in(A,B,C,D) -> evalperfectbb8in(A,A,-1 + A,D) [-2 + A >= 0] (?,1) 4. evalperfectbb8in(A,B,C,D) -> evalperfectbb4in(A,B,C,A) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1] (?,1) 5. evalperfectbb8in(A,B,C,D) -> evalperfectbb9in(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] (?,1) 6. evalperfectbb4in(A,B,C,D) -> evalperfectbb3in(A,B,C,D) [A + -1*D >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= C] 7. evalperfectbb4in(A,B,C,D) -> evalperfectbb5in(A,B,C,D) [A + -1*D >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] 8. evalperfectbb3in(A,B,C,D) -> evalperfectbb4in(A,B,C,-1*C + D) [A + -1*D >= 0 (?,1) && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] 9. evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 (?,1) && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] 10. evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 (?,1) && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] 11. evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 (?,1) && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= 1] 12. evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 0 >= 1 + A] (?,1) 13. evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1] (?,1) 14. evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = 0] (?,1) 15. evalperfectreturnin(A,B,C,D) -> evalperfectstop(A,B,C,D) True (?,1) Signature: {(evalperfectbb1in,4) ;(evalperfectbb3in,4) ;(evalperfectbb4in,4) ;(evalperfectbb5in,4) ;(evalperfectbb8in,4) ;(evalperfectbb9in,4) ;(evalperfectentryin,4) ;(evalperfectreturnin,4) ;(evalperfectstart,4) ;(evalperfectstop,4)} Flow Graph: [0->{1,2},1->{15},2->{3},3->{4,5},4->{6,7},5->{12,13,14},6->{8},7->{9,10,11},8->{6,7},9->{4,5},10->{4,5} ,11->{4,5},12->{15},13->{15},14->{15},15->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,5),(4,7),(11,5)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalperfectstart(A,B,C,D) -> evalperfectentryin(A,B,C,D) True (1,1) 1. evalperfectentryin(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [1 >= A] (?,1) 2. evalperfectentryin(A,B,C,D) -> evalperfectbb1in(A,B,C,D) [A >= 2] (?,1) 3. evalperfectbb1in(A,B,C,D) -> evalperfectbb8in(A,A,-1 + A,D) [-2 + A >= 0] (?,1) 4. evalperfectbb8in(A,B,C,D) -> evalperfectbb4in(A,B,C,A) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1] (?,1) 5. evalperfectbb8in(A,B,C,D) -> evalperfectbb9in(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] (?,1) 6. evalperfectbb4in(A,B,C,D) -> evalperfectbb3in(A,B,C,D) [A + -1*D >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= C] 7. evalperfectbb4in(A,B,C,D) -> evalperfectbb5in(A,B,C,D) [A + -1*D >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] 8. evalperfectbb3in(A,B,C,D) -> evalperfectbb4in(A,B,C,-1*C + D) [A + -1*D >= 0 (?,1) && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] 9. evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 (?,1) && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] 10. evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 (?,1) && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] 11. evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 (?,1) && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= 1] 12. evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 0 >= 1 + A] (?,1) 13. evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1] (?,1) 14. evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = 0] (?,1) 15. evalperfectreturnin(A,B,C,D) -> evalperfectstop(A,B,C,D) True (?,1) Signature: {(evalperfectbb1in,4) ;(evalperfectbb3in,4) ;(evalperfectbb4in,4) ;(evalperfectbb5in,4) ;(evalperfectbb8in,4) ;(evalperfectbb9in,4) ;(evalperfectentryin,4) ;(evalperfectreturnin,4) ;(evalperfectstart,4) ;(evalperfectstop,4)} Flow Graph: [0->{1,2},1->{15},2->{3},3->{4},4->{6},5->{12,13,14},6->{8},7->{9,10,11},8->{6,7},9->{4,5},10->{4,5} ,11->{4},12->{15},13->{15},14->{15},15->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalperfectstart(A,B,C,D) -> evalperfectentryin(A,B,C,D) True evalperfectentryin(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [1 >= A] evalperfectentryin(A,B,C,D) -> evalperfectbb1in(A,B,C,D) [A >= 2] evalperfectbb1in(A,B,C,D) -> evalperfectbb8in(A,A,-1 + A,D) [-2 + A >= 0] evalperfectbb8in(A,B,C,D) -> evalperfectbb4in(A,B,C,A) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1] evalperfectbb8in(A,B,C,D) -> evalperfectbb9in(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb4in(A,B,C,D) -> evalperfectbb3in(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= C] evalperfectbb4in(A,B,C,D) -> evalperfectbb5in(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb3in(A,B,C,D) -> evalperfectbb4in(A,B,C,-1*C + D) [A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= 1] evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 0 >= 1 + A] evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1] evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = 0] evalperfectreturnin(A,B,C,D) -> evalperfectstop(A,B,C,D) True Signature: {(evalperfectbb1in,4) ;(evalperfectbb3in,4) ;(evalperfectbb4in,4) ;(evalperfectbb5in,4) ;(evalperfectbb8in,4) ;(evalperfectbb9in,4) ;(evalperfectentryin,4) ;(evalperfectreturnin,4) ;(evalperfectstart,4) ;(evalperfectstop,4)} Rule Graph: [0->{1,2},1->{15},2->{3},3->{4},4->{6},5->{12,13,14},6->{8},7->{9,10,11},8->{6,7},9->{4,5},10->{4,5} ,11->{4},12->{15},13->{15},14->{15},15->{}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalperfectstart(A,B,C,D) -> evalperfectentryin(A,B,C,D) True evalperfectentryin(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [1 >= A] evalperfectentryin(A,B,C,D) -> evalperfectbb1in(A,B,C,D) [A >= 2] evalperfectbb1in(A,B,C,D) -> evalperfectbb8in(A,A,-1 + A,D) [-2 + A >= 0] evalperfectbb8in(A,B,C,D) -> evalperfectbb4in(A,B,C,A) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1] evalperfectbb8in(A,B,C,D) -> evalperfectbb9in(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb4in(A,B,C,D) -> evalperfectbb3in(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= C] evalperfectbb4in(A,B,C,D) -> evalperfectbb5in(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb3in(A,B,C,D) -> evalperfectbb4in(A,B,C,-1*C + D) [A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] evalperfectbb5in(A,B,C,D) -> evalperfectbb8in(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= 1] evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 0 >= 1 + A] evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1] evalperfectbb9in(A,B,C,D) -> evalperfectreturnin(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = 0] evalperfectreturnin(A,B,C,D) -> evalperfectstop(A,B,C,D) True evalperfectstop(A,B,C,D) -> exitus616(A,B,C,D) True evalperfectstop(A,B,C,D) -> exitus616(A,B,C,D) True evalperfectstop(A,B,C,D) -> exitus616(A,B,C,D) True evalperfectstop(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalperfectbb1in,4) ;(evalperfectbb3in,4) ;(evalperfectbb4in,4) ;(evalperfectbb5in,4) ;(evalperfectbb8in,4) ;(evalperfectbb9in,4) ;(evalperfectentryin,4) ;(evalperfectreturnin,4) ;(evalperfectstart,4) ;(evalperfectstop,4) ;(exitus616,4)} Rule Graph: [0->{1,2},1->{15},2->{3},3->{4},4->{6},5->{12,13,14},6->{8},7->{9,10,11},8->{6,7},9->{4,5},10->{4,5} ,11->{4},12->{15},13->{15},14->{15},15->{16,17,18,19}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalperfectstart.0(A,B,C,D) -> evalperfectentryin.1(A,B,C,D) True evalperfectstart.0(A,B,C,D) -> evalperfectentryin.2(A,B,C,D) True evalperfectentryin.1(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [1 >= A] evalperfectentryin.2(A,B,C,D) -> evalperfectbb1in.3(A,B,C,D) [A >= 2] evalperfectbb1in.3(A,B,C,D) -> evalperfectbb8in.4(A,A,-1 + A,D) [-2 + A >= 0] evalperfectbb8in.4(A,B,C,D) -> evalperfectbb4in.6(A,B,C,A) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1] evalperfectbb8in.5(A,B,C,D) -> evalperfectbb9in.12(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb8in.5(A,B,C,D) -> evalperfectbb9in.13(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb8in.5(A,B,C,D) -> evalperfectbb9in.14(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb4in.6(A,B,C,D) -> evalperfectbb3in.8(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= C] evalperfectbb4in.7(A,B,C,D) -> evalperfectbb5in.9(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb4in.7(A,B,C,D) -> evalperfectbb5in.10(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb4in.7(A,B,C,D) -> evalperfectbb5in.11(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb3in.8(A,B,C,D) -> evalperfectbb4in.6(A,B,C,-1*C + D) [A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] evalperfectbb3in.8(A,B,C,D) -> evalperfectbb4in.7(A,B,C,-1*C + D) [A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] evalperfectbb5in.9(A,B,C,D) -> evalperfectbb8in.4(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] evalperfectbb5in.9(A,B,C,D) -> evalperfectbb8in.5(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] evalperfectbb5in.10(A,B,C,D) -> evalperfectbb8in.4(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] evalperfectbb5in.10(A,B,C,D) -> evalperfectbb8in.5(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] evalperfectbb5in.11(A,B,C,D) -> evalperfectbb8in.4(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= 1] evalperfectbb9in.12(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 0 >= 1 + A] evalperfectbb9in.13(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1] evalperfectbb9in.14(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = 0] evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.16(A,B,C,D) True evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.17(A,B,C,D) True evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.18(A,B,C,D) True evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.19(A,B,C,D) True evalperfectstop.16(A,B,C,D) -> exitus616.20(A,B,C,D) True evalperfectstop.17(A,B,C,D) -> exitus616.20(A,B,C,D) True evalperfectstop.18(A,B,C,D) -> exitus616.20(A,B,C,D) True evalperfectstop.19(A,B,C,D) -> exitus616.20(A,B,C,D) True Signature: {(evalperfectbb1in.3,4) ;(evalperfectbb3in.8,4) ;(evalperfectbb4in.6,4) ;(evalperfectbb4in.7,4) ;(evalperfectbb5in.10,4) ;(evalperfectbb5in.11,4) ;(evalperfectbb5in.9,4) ;(evalperfectbb8in.4,4) ;(evalperfectbb8in.5,4) ;(evalperfectbb9in.12,4) ;(evalperfectbb9in.13,4) ;(evalperfectbb9in.14,4) ;(evalperfectentryin.1,4) ;(evalperfectentryin.2,4) ;(evalperfectreturnin.15,4) ;(evalperfectstart.0,4) ;(evalperfectstop.16,4) ;(evalperfectstop.17,4) ;(evalperfectstop.18,4) ;(evalperfectstop.19,4) ;(exitus616.20,4)} Rule Graph: [0->{2},1->{3},2->{23,24,25,26},3->{4},4->{5},5->{9},6->{20},7->{21},8->{22},9->{13,14},10->{15,16} ,11->{17,18},12->{19},13->{9},14->{10,11,12},15->{5},16->{6,7,8},17->{5},18->{6,7,8},19->{5},20->{23,24,25 ,26},21->{23,24,25,26},22->{23,24,25,26},23->{27},24->{28},25->{29},26->{30},27->{},28->{},29->{},30->{}] + 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,23,24,25,26,27,28,29,30] | `- p:[5,15,10,14,9,13,17,11,19,12] c: [5,10,11,12,14,15,17,19] | `- p:[9,13] c: [9,13] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalperfectstart.0(A,B,C,D) -> evalperfectentryin.1(A,B,C,D) True evalperfectstart.0(A,B,C,D) -> evalperfectentryin.2(A,B,C,D) True evalperfectentryin.1(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [1 >= A] evalperfectentryin.2(A,B,C,D) -> evalperfectbb1in.3(A,B,C,D) [A >= 2] evalperfectbb1in.3(A,B,C,D) -> evalperfectbb8in.4(A,A,-1 + A,D) [-2 + A >= 0] evalperfectbb8in.4(A,B,C,D) -> evalperfectbb4in.6(A,B,C,A) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1] evalperfectbb8in.5(A,B,C,D) -> evalperfectbb9in.12(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb8in.5(A,B,C,D) -> evalperfectbb9in.13(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb8in.5(A,B,C,D) -> evalperfectbb9in.14(B,B,C,D) [-1 + A + -1*C >= 0 && C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= C] evalperfectbb4in.6(A,B,C,D) -> evalperfectbb3in.8(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= C] evalperfectbb4in.7(A,B,C,D) -> evalperfectbb5in.9(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb4in.7(A,B,C,D) -> evalperfectbb5in.10(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb4in.7(A,B,C,D) -> evalperfectbb5in.11(A,B,C,D) [A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && C >= 1 + D] evalperfectbb3in.8(A,B,C,D) -> evalperfectbb4in.6(A,B,C,-1*C + D) [A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] evalperfectbb3in.8(A,B,C,D) -> evalperfectbb4in.7(A,B,C,-1*C + D) [A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -3 + A + D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0] evalperfectbb5in.9(A,B,C,D) -> evalperfectbb8in.4(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] evalperfectbb5in.9(A,B,C,D) -> evalperfectbb8in.5(A,B + -1*C,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D = 0] evalperfectbb5in.10(A,B,C,D) -> evalperfectbb8in.4(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] evalperfectbb5in.10(A,B,C,D) -> evalperfectbb8in.5(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && 0 >= 1 + D] evalperfectbb5in.11(A,B,C,D) -> evalperfectbb8in.4(A,B,-1 + C,D) [-1 + C + -1*D >= 0 && -2 + A + -1*D >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + A >= 0 && D >= 1] evalperfectbb9in.12(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 0 >= 1 + A] evalperfectbb9in.13(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1] evalperfectbb9in.14(A,B,C,D) -> evalperfectreturnin.15(A,B,C,D) [-1*C >= 0 && C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = 0] evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.16(A,B,C,D) True evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.17(A,B,C,D) True evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.18(A,B,C,D) True evalperfectreturnin.15(A,B,C,D) -> evalperfectstop.19(A,B,C,D) True evalperfectstop.16(A,B,C,D) -> exitus616.20(A,B,C,D) True evalperfectstop.17(A,B,C,D) -> exitus616.20(A,B,C,D) True evalperfectstop.18(A,B,C,D) -> exitus616.20(A,B,C,D) True evalperfectstop.19(A,B,C,D) -> exitus616.20(A,B,C,D) True Signature: {(evalperfectbb1in.3,4) ;(evalperfectbb3in.8,4) ;(evalperfectbb4in.6,4) ;(evalperfectbb4in.7,4) ;(evalperfectbb5in.10,4) ;(evalperfectbb5in.11,4) ;(evalperfectbb5in.9,4) ;(evalperfectbb8in.4,4) ;(evalperfectbb8in.5,4) ;(evalperfectbb9in.12,4) ;(evalperfectbb9in.13,4) ;(evalperfectbb9in.14,4) ;(evalperfectentryin.1,4) ;(evalperfectentryin.2,4) ;(evalperfectreturnin.15,4) ;(evalperfectstart.0,4) ;(evalperfectstop.16,4) ;(evalperfectstop.17,4) ;(evalperfectstop.18,4) ;(evalperfectstop.19,4) ;(exitus616.20,4)} Rule Graph: [0->{2},1->{3},2->{23,24,25,26},3->{4},4->{5},5->{9},6->{20},7->{21},8->{22},9->{13,14},10->{15,16} ,11->{17,18},12->{19},13->{9},14->{10,11,12},15->{5},16->{6,7,8},17->{5},18->{6,7,8},19->{5},20->{23,24,25 ,26},21->{23,24,25,26},22->{23,24,25,26},23->{27},24->{28},25->{29},26->{30},27->{},28->{},29->{},30->{}] ,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,28,29,30] | `- p:[5,15,10,14,9,13,17,11,19,12] c: [5,10,11,12,14,15,17,19] | `- p:[9,13] c: [9,13]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalperfectstart.0 ~> evalperfectentryin.1 [A <= A, B <= B, C <= C, D <= D] evalperfectstart.0 ~> evalperfectentryin.2 [A <= A, B <= B, C <= C, D <= D] evalperfectentryin.1 ~> evalperfectreturnin.15 [A <= A, B <= B, C <= C, D <= D] evalperfectentryin.2 ~> evalperfectbb1in.3 [A <= A, B <= B, C <= C, D <= D] evalperfectbb1in.3 ~> evalperfectbb8in.4 [A <= A, B <= A, C <= A, D <= D] evalperfectbb8in.4 ~> evalperfectbb4in.6 [A <= A, B <= B, C <= C, D <= A] evalperfectbb8in.5 ~> evalperfectbb9in.12 [A <= B, B <= B, C <= C, D <= D] evalperfectbb8in.5 ~> evalperfectbb9in.13 [A <= B, B <= B, C <= C, D <= D] evalperfectbb8in.5 ~> evalperfectbb9in.14 [A <= B, B <= B, C <= C, D <= D] evalperfectbb4in.6 ~> evalperfectbb3in.8 [A <= A, B <= B, C <= C, D <= D] evalperfectbb4in.7 ~> evalperfectbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalperfectbb4in.7 ~> evalperfectbb5in.10 [A <= A, B <= B, C <= C, D <= D] evalperfectbb4in.7 ~> evalperfectbb5in.11 [A <= A, B <= B, C <= C, D <= D] evalperfectbb3in.8 ~> evalperfectbb4in.6 [A <= A, B <= B, C <= C, D <= A] evalperfectbb3in.8 ~> evalperfectbb4in.7 [A <= A, B <= B, C <= C, D <= A] evalperfectbb5in.9 ~> evalperfectbb8in.4 [A <= A, B <= B + C, C <= C, D <= D] evalperfectbb5in.9 ~> evalperfectbb8in.5 [A <= A, B <= B + C, C <= C, D <= D] evalperfectbb5in.10 ~> evalperfectbb8in.4 [A <= A, B <= B, C <= C, D <= D] evalperfectbb5in.10 ~> evalperfectbb8in.5 [A <= A, B <= B, C <= C, D <= D] evalperfectbb5in.11 ~> evalperfectbb8in.4 [A <= A, B <= B, C <= C, D <= D] evalperfectbb9in.12 ~> evalperfectreturnin.15 [A <= A, B <= B, C <= C, D <= D] evalperfectbb9in.13 ~> evalperfectreturnin.15 [A <= A, B <= B, C <= C, D <= D] evalperfectbb9in.14 ~> evalperfectreturnin.15 [A <= A, B <= B, C <= C, D <= D] evalperfectreturnin.15 ~> evalperfectstop.16 [A <= A, B <= B, C <= C, D <= D] evalperfectreturnin.15 ~> evalperfectstop.17 [A <= A, B <= B, C <= C, D <= D] evalperfectreturnin.15 ~> evalperfectstop.18 [A <= A, B <= B, C <= C, D <= D] evalperfectreturnin.15 ~> evalperfectstop.19 [A <= A, B <= B, C <= C, D <= D] evalperfectstop.16 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D] evalperfectstop.17 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D] evalperfectstop.18 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D] evalperfectstop.19 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + C] evalperfectbb8in.4 ~> evalperfectbb4in.6 [A <= A, B <= B, C <= C, D <= A] evalperfectbb5in.9 ~> evalperfectbb8in.4 [A <= A, B <= B + C, C <= C, D <= D] evalperfectbb4in.7 ~> evalperfectbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalperfectbb3in.8 ~> evalperfectbb4in.7 [A <= A, B <= B, C <= C, D <= A] evalperfectbb4in.6 ~> evalperfectbb3in.8 [A <= A, B <= B, C <= C, D <= D] evalperfectbb3in.8 ~> evalperfectbb4in.6 [A <= A, B <= B, C <= C, D <= A] evalperfectbb5in.10 ~> evalperfectbb8in.4 [A <= A, B <= B, C <= C, D <= D] evalperfectbb4in.7 ~> evalperfectbb5in.10 [A <= A, B <= B, C <= C, D <= D] evalperfectbb5in.11 ~> evalperfectbb8in.4 [A <= A, B <= B, C <= C, D <= D] evalperfectbb4in.7 ~> evalperfectbb5in.11 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + D] evalperfectbb4in.6 ~> evalperfectbb3in.8 [A <= A, B <= B, C <= C, D <= D] evalperfectbb3in.8 ~> evalperfectbb4in.6 [A <= A, B <= B, C <= C, D <= A] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalperfectstart.0 ~> evalperfectentryin.1 [] evalperfectstart.0 ~> evalperfectentryin.2 [] evalperfectentryin.1 ~> evalperfectreturnin.15 [] evalperfectentryin.2 ~> evalperfectbb1in.3 [] evalperfectbb1in.3 ~> evalperfectbb8in.4 [A ~=> B,A ~=> C] evalperfectbb8in.4 ~> evalperfectbb4in.6 [A ~=> D] evalperfectbb8in.5 ~> evalperfectbb9in.12 [B ~=> A] evalperfectbb8in.5 ~> evalperfectbb9in.13 [B ~=> A] evalperfectbb8in.5 ~> evalperfectbb9in.14 [B ~=> A] evalperfectbb4in.6 ~> evalperfectbb3in.8 [] evalperfectbb4in.7 ~> evalperfectbb5in.9 [] evalperfectbb4in.7 ~> evalperfectbb5in.10 [] evalperfectbb4in.7 ~> evalperfectbb5in.11 [] evalperfectbb3in.8 ~> evalperfectbb4in.6 [A ~=> D] evalperfectbb3in.8 ~> evalperfectbb4in.7 [A ~=> D] evalperfectbb5in.9 ~> evalperfectbb8in.4 [B ~+> B,C ~+> B] evalperfectbb5in.9 ~> evalperfectbb8in.5 [B ~+> B,C ~+> B] evalperfectbb5in.10 ~> evalperfectbb8in.4 [] evalperfectbb5in.10 ~> evalperfectbb8in.5 [] evalperfectbb5in.11 ~> evalperfectbb8in.4 [] evalperfectbb9in.12 ~> evalperfectreturnin.15 [] evalperfectbb9in.13 ~> evalperfectreturnin.15 [] evalperfectbb9in.14 ~> evalperfectreturnin.15 [] evalperfectreturnin.15 ~> evalperfectstop.16 [] evalperfectreturnin.15 ~> evalperfectstop.17 [] evalperfectreturnin.15 ~> evalperfectstop.18 [] evalperfectreturnin.15 ~> evalperfectstop.19 [] evalperfectstop.16 ~> exitus616.20 [] evalperfectstop.17 ~> exitus616.20 [] evalperfectstop.18 ~> exitus616.20 [] evalperfectstop.19 ~> exitus616.20 [] + Loop: [C ~+> 0.0,K ~+> 0.0] evalperfectbb8in.4 ~> evalperfectbb4in.6 [A ~=> D] evalperfectbb5in.9 ~> evalperfectbb8in.4 [B ~+> B,C ~+> B] evalperfectbb4in.7 ~> evalperfectbb5in.9 [] evalperfectbb3in.8 ~> evalperfectbb4in.7 [A ~=> D] evalperfectbb4in.6 ~> evalperfectbb3in.8 [] evalperfectbb3in.8 ~> evalperfectbb4in.6 [A ~=> D] evalperfectbb5in.10 ~> evalperfectbb8in.4 [] evalperfectbb4in.7 ~> evalperfectbb5in.10 [] evalperfectbb5in.11 ~> evalperfectbb8in.4 [] evalperfectbb4in.7 ~> evalperfectbb5in.11 [] + Loop: [D ~+> 0.0.0,K ~+> 0.0.0] evalperfectbb4in.6 ~> evalperfectbb3in.8 [] evalperfectbb3in.8 ~> evalperfectbb4in.6 [A ~=> D] + Applied Processor: Lare + Details: evalperfectstart.0 ~> exitus616.20 [A ~=> B ,A ~=> C ,A ~=> D ,A ~+> A ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> tick] + evalperfectbb5in.9> [A ~=> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,C ~+> B ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,C ~*> B ,C ~*> tick ,K ~*> B ,K ~*> tick] evalperfectbb5in.10> [A ~=> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,C ~+> B ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,C ~*> B ,C ~*> tick ,K ~*> B ,K ~*> tick] + evalperfectbb3in.8> [A ~=> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick] YES(?,POLY)