YES(?,PRIMREC) * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> f2(A,B,C,D,E,F,G,H) True (1,1) 1. f2(A,B,C,D,E,F,G,H) -> f1(A,B,C,D,E,F,G,H) [B >= A] (?,1) 2. f2(A,B,C,D,E,F,G,H) -> f8(A,B,0,B,E,F,G,H) [A >= 1 + B] (?,1) 3. f8(A,B,C,D,E,F,G,H) -> f34(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] (?,1) 4. f8(A,B,C,D,E,F,G,H) -> f8(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] (?,1) 5. f8(A,B,C,D,E,F,G,H) -> f8(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] (?,1) 6. f34(A,B,C,D,E,F,G,H) -> f2(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] (?,1) 7. f34(A,B,C,D,E,F,G,H) -> f36(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] (?,1) 8. f34(A,B,C,D,E,F,G,H) -> f36(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] (?,1) 9. f8(A,B,C,D,E,F,G,H) -> f19(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] (?,1) 10. f8(A,B,C,D,E,F,G,H) -> f19(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] (?,1) 11. f19(A,B,C,D,E,F,G,H) -> f27(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 12. f36(A,B,C,D,E,F,G,H) -> f2(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] (?,1) 13. f36(A,B,C,D,E,F,G,H) -> f36(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] (?,1) 14. f36(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 (?,1) && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] 15. f36(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 (?,1) && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] 16. f27(A,B,C,D,E,F,G,H) -> f34(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 17. f43(A,B,C,D,E,F,G,H) -> f49(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] 18. f49(A,B,C,D,E,F,G,H) -> f36(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f1,8);(f19,8);(f2,8);(f27,8);(f34,8);(f36,8);(f43,8);(f49,8);(f8,8);(start,8)} Flow Graph: [0->{1,2},1->{},2->{3,4,5,9,10},3->{6,7,8},4->{3,4,5,9,10},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15} ,8->{12,13,14,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8} ,17->{18},18->{12,13,14,15}] + Applied Processor: ArgumentFilter [5,6,7] + Details: We remove following argument positions: [5,6,7]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E) -> f2(A,B,C,D,E) True (1,1) 1. f2(A,B,C,D,E) -> f1(A,B,C,D,E) [B >= A] (?,1) 2. f2(A,B,C,D,E) -> f8(A,B,0,B,E) [A >= 1 + B] (?,1) 3. f8(A,B,C,D,E) -> f34(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] (?,1) 4. f8(A,B,C,D,E) -> f8(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] (?,1) 5. f8(A,B,C,D,E) -> f8(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] (?,1) 6. f34(A,B,C,D,E) -> f2(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] (?,1) 7. f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] (?,1) 8. f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] (?,1) 9. f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] (?,1) 10. f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] (?,1) 11. f19(A,B,C,D,E) -> f27(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 12. f36(A,B,C,D,E) -> f2(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] (?,1) 13. f36(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] (?,1) 14. f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 (?,1) && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] 15. f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 (?,1) && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] 16. f27(A,B,C,D,E) -> f34(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 17. f43(A,B,C,D,E) -> f49(A,B,C,D,E) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] 18. f49(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f1,8);(f19,8);(f2,8);(f27,8);(f34,8);(f36,8);(f43,8);(f49,8);(f8,8);(start,8)} Flow Graph: [0->{1,2},1->{},2->{3,4,5,9,10},3->{6,7,8},4->{3,4,5,9,10},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15} ,8->{12,13,14,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8} ,17->{18},18->{12,13,14,15}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(2,10),(4,3),(4,10)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E) -> f2(A,B,C,D,E) True (1,1) 1. f2(A,B,C,D,E) -> f1(A,B,C,D,E) [B >= A] (?,1) 2. f2(A,B,C,D,E) -> f8(A,B,0,B,E) [A >= 1 + B] (?,1) 3. f8(A,B,C,D,E) -> f34(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] (?,1) 4. f8(A,B,C,D,E) -> f8(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] (?,1) 5. f8(A,B,C,D,E) -> f8(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] (?,1) 6. f34(A,B,C,D,E) -> f2(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] (?,1) 7. f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] (?,1) 8. f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] (?,1) 9. f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] (?,1) 10. f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] (?,1) 11. f19(A,B,C,D,E) -> f27(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 12. f36(A,B,C,D,E) -> f2(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] (?,1) 13. f36(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] (?,1) 14. f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 (?,1) && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] 15. f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 (?,1) && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] 16. f27(A,B,C,D,E) -> f34(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 17. f43(A,B,C,D,E) -> f49(A,B,C,D,E) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] 18. f49(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f1,8);(f19,8);(f2,8);(f27,8);(f34,8);(f36,8);(f43,8);(f49,8);(f8,8);(start,8)} Flow Graph: [0->{1,2},1->{},2->{3,4,5},3->{6,7,8},4->{4,5,9},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15},8->{12,13,14 ,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8},17->{18},18->{12,13 ,14,15}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: start(A,B,C,D,E) -> f2(A,B,C,D,E) True f2(A,B,C,D,E) -> f1(A,B,C,D,E) [B >= A] f2(A,B,C,D,E) -> f8(A,B,0,B,E) [A >= 1 + B] f8(A,B,C,D,E) -> f34(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8(A,B,C,D,E) -> f8(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8(A,B,C,D,E) -> f8(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f34(A,B,C,D,E) -> f2(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f19(A,B,C,D,E) -> f27(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f36(A,B,C,D,E) -> f2(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f36(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f27(A,B,C,D,E) -> f34(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43(A,B,C,D,E) -> f49(A,B,C,D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f1,8);(f19,8);(f2,8);(f27,8);(f34,8);(f36,8);(f43,8);(f49,8);(f8,8);(start,8)} Rule Graph: [0->{1,2},1->{},2->{3,4,5},3->{6,7,8},4->{4,5,9},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15},8->{12,13,14 ,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8},17->{18},18->{12,13 ,14,15}] + Applied Processor: AddSinks + Details: () * Step 5: Unfold MAYBE + Considered Problem: Rules: start(A,B,C,D,E) -> f2(A,B,C,D,E) True f2(A,B,C,D,E) -> f1(A,B,C,D,E) [B >= A] f2(A,B,C,D,E) -> f8(A,B,0,B,E) [A >= 1 + B] f8(A,B,C,D,E) -> f34(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8(A,B,C,D,E) -> f8(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8(A,B,C,D,E) -> f8(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f34(A,B,C,D,E) -> f2(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34(A,B,C,D,E) -> f36(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f8(A,B,C,D,E) -> f19(A,B,C,D,E) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f19(A,B,C,D,E) -> f27(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f36(A,B,C,D,E) -> f2(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f36(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f36(A,B,C,D,E) -> f43(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f27(A,B,C,D,E) -> f34(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43(A,B,C,D,E) -> f49(A,B,C,D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49(A,B,C,D,E) -> f36(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f1(A,B,C,D,E) -> exitus616(A,B,C,D,E) True Signature: {(exitus616,5);(f1,8);(f19,8);(f2,8);(f27,8);(f34,8);(f36,8);(f43,8);(f49,8);(f8,8);(start,8)} Rule Graph: [0->{1,2},1->{19},2->{3,4,5},3->{6,7,8},4->{4,5,9},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15},8->{12,13,14 ,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8},17->{18},18->{12,13 ,14,15}] + Applied Processor: Unfold + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E) -> f2.1(A,B,C,D,E) True start.0(A,B,C,D,E) -> f2.2(A,B,C,D,E) True f2.1(A,B,C,D,E) -> f1.19(A,B,C,D,E) [B >= A] f2.2(A,B,C,D,E) -> f8.3(A,B,0,B,E) [A >= 1 + B] f2.2(A,B,C,D,E) -> f8.4(A,B,0,B,E) [A >= 1 + B] f2.2(A,B,C,D,E) -> f8.5(A,B,0,B,E) [A >= 1 + B] f8.3(A,B,C,D,E) -> f34.6(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8.3(A,B,C,D,E) -> f34.7(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8.3(A,B,C,D,E) -> f34.8(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8.4(A,B,C,D,E) -> f8.4(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8.4(A,B,C,D,E) -> f8.5(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8.4(A,B,C,D,E) -> f8.9(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8.5(A,B,C,D,E) -> f8.3(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.4(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.5(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.9(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.10(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f34.6(A,B,C,D,E) -> f2.1(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f34.6(A,B,C,D,E) -> f2.2(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f34.7(A,B,C,D,E) -> f36.12(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.7(A,B,C,D,E) -> f36.13(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.7(A,B,C,D,E) -> f36.14(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.7(A,B,C,D,E) -> f36.15(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.8(A,B,C,D,E) -> f36.12(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f34.8(A,B,C,D,E) -> f36.13(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f34.8(A,B,C,D,E) -> f36.14(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f34.8(A,B,C,D,E) -> f36.15(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f8.9(A,B,C,D,E) -> f19.11(A,B,C,D,E) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f8.10(A,B,C,D,E) -> f19.11(A,B,C,D,E) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f19.11(A,B,C,D,E) -> f27.16(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f36.12(A,B,C,D,E) -> f2.1(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f36.12(A,B,C,D,E) -> f2.2(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f36.13(A,B,C,D,E) -> f36.12(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.13(A,B,C,D,E) -> f36.13(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.13(A,B,C,D,E) -> f36.14(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.13(A,B,C,D,E) -> f36.15(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.14(A,B,C,D,E) -> f43.17(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f36.15(A,B,C,D,E) -> f43.17(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f27.16(A,B,C,D,E) -> f34.6(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f27.16(A,B,C,D,E) -> f34.7(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f27.16(A,B,C,D,E) -> f34.8(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43.17(A,B,C,D,E) -> f49.18(A,B,C,D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.12(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.13(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.14(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.15(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f1.19(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True Signature: {(exitus616.20,5) ;(f1.19,5) ;(f19.11,5) ;(f2.1,5) ;(f2.2,5) ;(f27.16,5) ;(f34.6,5) ;(f34.7,5) ;(f34.8,5) ;(f36.12,5) ;(f36.13,5) ;(f36.14,5) ;(f36.15,5) ;(f43.17,5) ;(f49.18,5) ;(f8.10,5) ;(f8.3,5) ;(f8.4,5) ;(f8.5,5) ;(f8.9,5) ;(start.0,5)} Rule Graph: [0->{2},1->{3,4,5},2->{46},3->{6,7,8},4->{9,10,11},5->{12,13,14,15,16},6->{17,18},7->{19,20,21,22},8->{23 ,24,25,26},9->{9,10,11},10->{12,13,14,15,16},11->{27},12->{6,7,8},13->{9,10,11},14->{12,13,14,15,16} ,15->{27},16->{28},17->{2},18->{3,4,5},19->{30,31},20->{32,33,34,35},21->{36},22->{37},23->{30,31},24->{32 ,33,34,35},25->{36},26->{37},27->{29},28->{29},29->{38,39,40},30->{2},31->{3,4,5},32->{30,31},33->{32,33,34 ,35},34->{36},35->{37},36->{41},37->{41},38->{17,18},39->{19,20,21,22},40->{23,24,25,26},41->{42,43,44,45} ,42->{30,31},43->{32,33,34,35},44->{36},45->{37},46->{}] + 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,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46] | `- p:[3,18,6,12,5,31,19,7,39,29,27,11,4,9,13,10,14,15,28,16,23,8,40,32,20,24,33,43,41,36,21,25,34,44,37,22,26,35,45,42,38] c: [3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,31,32,38,39,40,42] | `- p:[33,43,41,36,34,44,37,35,45] c: [33,34,35,36,37,41,43,44,45] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: start.0(A,B,C,D,E) -> f2.1(A,B,C,D,E) True start.0(A,B,C,D,E) -> f2.2(A,B,C,D,E) True f2.1(A,B,C,D,E) -> f1.19(A,B,C,D,E) [B >= A] f2.2(A,B,C,D,E) -> f8.3(A,B,0,B,E) [A >= 1 + B] f2.2(A,B,C,D,E) -> f8.4(A,B,0,B,E) [A >= 1 + B] f2.2(A,B,C,D,E) -> f8.5(A,B,0,B,E) [A >= 1 + B] f8.3(A,B,C,D,E) -> f34.6(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8.3(A,B,C,D,E) -> f34.7(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8.3(A,B,C,D,E) -> f34.8(A,B,C,B,E) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f8.4(A,B,C,D,E) -> f8.4(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8.4(A,B,C,D,E) -> f8.5(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8.4(A,B,C,D,E) -> f8.9(A,B,J,E,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f8.5(A,B,C,D,E) -> f8.3(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.4(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.5(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.9(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f8.5(A,B,C,D,E) -> f8.10(A,B,C,D,1 + E) [-1 + A + -1*B >= 0 && A >= E && I >= J] f34.6(A,B,C,D,E) -> f2.1(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f34.6(A,B,C,D,E) -> f2.2(A,1 + B,0,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f34.7(A,B,C,D,E) -> f36.12(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.7(A,B,C,D,E) -> f36.13(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.7(A,B,C,D,E) -> f36.14(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.7(A,B,C,D,E) -> f36.15(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f34.8(A,B,C,D,E) -> f36.12(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f34.8(A,B,C,D,E) -> f36.13(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f34.8(A,B,C,D,E) -> f36.14(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f34.8(A,B,C,D,E) -> f36.15(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f8.9(A,B,C,D,E) -> f19.11(A,B,C,D,E) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f8.10(A,B,C,D,E) -> f19.11(A,B,C,D,E) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f19.11(A,B,C,D,E) -> f27.16(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f36.12(A,B,C,D,E) -> f2.1(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f36.12(A,B,C,D,E) -> f2.2(A,1 + B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f36.13(A,B,C,D,E) -> f36.12(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.13(A,B,C,D,E) -> f36.13(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.13(A,B,C,D,E) -> f36.14(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.13(A,B,C,D,E) -> f36.15(A,B,C,1 + D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f36.14(A,B,C,D,E) -> f43.17(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && I >= 1 && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f36.15(A,B,C,D,E) -> f43.17(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + I && A >= D && I >= C*K && C*K + K >= 1 + I && K >= J && I >= C*L && C*L + L >= 1 + I && J >= L] f27.16(A,B,C,D,E) -> f34.6(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f27.16(A,B,C,D,E) -> f34.7(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f27.16(A,B,C,D,E) -> f34.8(A,B,C,D,E) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43.17(A,B,C,D,E) -> f49.18(A,B,C,D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.12(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.13(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.14(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f49.18(A,B,C,D,E) -> f36.15(A,B,C,1 + D,E) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f1.19(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True Signature: {(exitus616.20,5) ;(f1.19,5) ;(f19.11,5) ;(f2.1,5) ;(f2.2,5) ;(f27.16,5) ;(f34.6,5) ;(f34.7,5) ;(f34.8,5) ;(f36.12,5) ;(f36.13,5) ;(f36.14,5) ;(f36.15,5) ;(f43.17,5) ;(f49.18,5) ;(f8.10,5) ;(f8.3,5) ;(f8.4,5) ;(f8.5,5) ;(f8.9,5) ;(start.0,5)} Rule Graph: [0->{2},1->{3,4,5},2->{46},3->{6,7,8},4->{9,10,11},5->{12,13,14,15,16},6->{17,18},7->{19,20,21,22},8->{23 ,24,25,26},9->{9,10,11},10->{12,13,14,15,16},11->{27},12->{6,7,8},13->{9,10,11},14->{12,13,14,15,16} ,15->{27},16->{28},17->{2},18->{3,4,5},19->{30,31},20->{32,33,34,35},21->{36},22->{37},23->{30,31},24->{32 ,33,34,35},25->{36},26->{37},27->{29},28->{29},29->{38,39,40},30->{2},31->{3,4,5},32->{30,31},33->{32,33,34 ,35},34->{36},35->{37},36->{41},37->{41},38->{17,18},39->{19,20,21,22},40->{23,24,25,26},41->{42,43,44,45} ,42->{30,31},43->{32,33,34,35},44->{36},45->{37},46->{}] ,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,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46] | `- p:[3,18,6,12,5,31,19,7,39,29,27,11,4,9,13,10,14,15,28,16,23,8,40,32,20,24,33,43,41,36,21,25,34,44,37,22,26,35,45,42,38] c: [3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,31,32,38,39,40,42] | `- p:[33,43,41,36,34,44,37,35,45] c: [33,34,35,36,37,41,43,44,45]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.0.0] start.0 ~> f2.1 [A <= A, B <= B, C <= C, D <= D, E <= E] start.0 ~> f2.2 [A <= A, B <= B, C <= C, D <= D, E <= E] f2.1 ~> f1.19 [A <= A, B <= B, C <= C, D <= D, E <= E] f2.2 ~> f8.3 [A <= A, B <= B, C <= 0*K, D <= B, E <= E] f2.2 ~> f8.4 [A <= A, B <= B, C <= 0*K, D <= B, E <= E] f2.2 ~> f8.5 [A <= A, B <= B, C <= 0*K, D <= B, E <= E] f8.3 ~> f34.6 [A <= A, B <= B, C <= C, D <= B, E <= E] f8.3 ~> f34.7 [A <= A, B <= B, C <= C, D <= B, E <= E] f8.3 ~> f34.8 [A <= A, B <= B, C <= C, D <= B, E <= E] f8.4 ~> f8.4 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E] f8.4 ~> f8.5 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E] f8.4 ~> f8.9 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E] f8.5 ~> f8.3 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.5 ~> f8.4 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.5 ~> f8.5 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.5 ~> f8.9 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.5 ~> f8.10 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f34.6 ~> f2.1 [A <= A, B <= B + E, C <= 0*K, D <= D, E <= E] f34.6 ~> f2.2 [A <= A, B <= B + E, C <= 0*K, D <= D, E <= E] f34.7 ~> f36.12 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.7 ~> f36.13 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.7 ~> f36.14 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.7 ~> f36.15 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.12 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.13 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.14 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.15 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.9 ~> f19.11 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.10 ~> f19.11 [A <= A, B <= B, C <= C, D <= D, E <= E] f19.11 ~> f27.16 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.12 ~> f2.1 [A <= A, B <= A + B, C <= C, D <= D, E <= E] f36.12 ~> f2.2 [A <= A, B <= A + B, C <= C, D <= D, E <= E] f36.13 ~> f36.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f36.13 ~> f36.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f36.13 ~> f36.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f36.13 ~> f36.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f36.14 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.15 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E] f27.16 ~> f34.6 [A <= A, B <= B, C <= C, D <= D, E <= E] f27.16 ~> f34.7 [A <= A, B <= B, C <= C, D <= D, E <= E] f27.16 ~> f34.8 [A <= A, B <= B, C <= C, D <= D, E <= E] f43.17 ~> f49.18 [A <= A, B <= B, C <= C, D <= D, E <= E] f49.18 ~> f36.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f1.19 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= K + A + B + E] f2.2 ~> f8.3 [A <= A, B <= B, C <= 0*K, D <= B, E <= E] f34.6 ~> f2.2 [A <= A, B <= B + E, C <= 0*K, D <= D, E <= E] f8.3 ~> f34.6 [A <= A, B <= B, C <= C, D <= B, E <= E] f8.5 ~> f8.3 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f2.2 ~> f8.5 [A <= A, B <= B, C <= 0*K, D <= B, E <= E] f36.12 ~> f2.2 [A <= A, B <= A + B, C <= C, D <= D, E <= E] f34.7 ~> f36.12 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.3 ~> f34.7 [A <= A, B <= B, C <= C, D <= B, E <= E] f27.16 ~> f34.7 [A <= A, B <= B, C <= C, D <= D, E <= E] f19.11 ~> f27.16 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.9 ~> f19.11 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.4 ~> f8.9 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E] f2.2 ~> f8.4 [A <= A, B <= B, C <= 0*K, D <= B, E <= E] f8.4 ~> f8.4 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E] f8.5 ~> f8.4 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.4 ~> f8.5 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E] f8.5 ~> f8.5 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.5 ~> f8.9 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f8.10 ~> f19.11 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.5 ~> f8.10 [A <= A, B <= B, C <= C, D <= D, E <= K + E] f34.8 ~> f36.12 [A <= A, B <= B, C <= C, D <= D, E <= E] f8.3 ~> f34.8 [A <= A, B <= B, C <= C, D <= B, E <= E] f27.16 ~> f34.8 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.13 ~> f36.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f34.7 ~> f36.13 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.13 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.13 ~> f36.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f43.17 ~> f49.18 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.14 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.7 ~> f36.14 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.14 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.13 ~> f36.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f36.15 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.7 ~> f36.15 [A <= A, B <= B, C <= C, D <= D, E <= E] f34.8 ~> f36.15 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.13 ~> f36.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f27.16 ~> f34.6 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0.0 <= K + A + D] f36.13 ~> f36.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f43.17 ~> f49.18 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.14 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.13 ~> f36.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f36.15 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E] f36.13 ~> f36.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f49.18 ~> f36.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.0.0] start.0 ~> f2.1 [] start.0 ~> f2.2 [] f2.1 ~> f1.19 [] f2.2 ~> f8.3 [B ~=> D,K ~=> C] f2.2 ~> f8.4 [B ~=> D,K ~=> C] f2.2 ~> f8.5 [B ~=> D,K ~=> C] f8.3 ~> f34.6 [B ~=> D] f8.3 ~> f34.7 [B ~=> D] f8.3 ~> f34.8 [B ~=> D] f8.4 ~> f8.4 [E ~=> D,huge ~=> C,E ~+> E,K ~+> E] f8.4 ~> f8.5 [E ~=> D,huge ~=> C,E ~+> E,K ~+> E] f8.4 ~> f8.9 [E ~=> D,huge ~=> C,E ~+> E,K ~+> E] f8.5 ~> f8.3 [E ~+> E,K ~+> E] f8.5 ~> f8.4 [E ~+> E,K ~+> E] f8.5 ~> f8.5 [E ~+> E,K ~+> E] f8.5 ~> f8.9 [E ~+> E,K ~+> E] f8.5 ~> f8.10 [E ~+> E,K ~+> E] f34.6 ~> f2.1 [K ~=> C,B ~+> B,E ~+> B] f34.6 ~> f2.2 [K ~=> C,B ~+> B,E ~+> B] f34.7 ~> f36.12 [] f34.7 ~> f36.13 [] f34.7 ~> f36.14 [] f34.7 ~> f36.15 [] f34.8 ~> f36.12 [] f34.8 ~> f36.13 [] f34.8 ~> f36.14 [] f34.8 ~> f36.15 [] f8.9 ~> f19.11 [] f8.10 ~> f19.11 [] f19.11 ~> f27.16 [] f36.12 ~> f2.1 [A ~+> B,B ~+> B] f36.12 ~> f2.2 [A ~+> B,B ~+> B] f36.13 ~> f36.12 [D ~+> D,E ~+> D] f36.13 ~> f36.13 [D ~+> D,E ~+> D] f36.13 ~> f36.14 [D ~+> D,E ~+> D] f36.13 ~> f36.15 [D ~+> D,E ~+> D] f36.14 ~> f43.17 [] f36.15 ~> f43.17 [] f27.16 ~> f34.6 [] f27.16 ~> f34.7 [] f27.16 ~> f34.8 [] f43.17 ~> f49.18 [] f49.18 ~> f36.12 [D ~+> D,E ~+> D] f49.18 ~> f36.13 [D ~+> D,E ~+> D] f49.18 ~> f36.14 [D ~+> D,E ~+> D] f49.18 ~> f36.15 [D ~+> D,E ~+> D] f1.19 ~> exitus616.20 [] + Loop: [A ~+> 0.0,B ~+> 0.0,E ~+> 0.0,K ~+> 0.0] f2.2 ~> f8.3 [B ~=> D,K ~=> C] f34.6 ~> f2.2 [K ~=> C,B ~+> B,E ~+> B] f8.3 ~> f34.6 [B ~=> D] f8.5 ~> f8.3 [E ~+> E,K ~+> E] f2.2 ~> f8.5 [B ~=> D,K ~=> C] f36.12 ~> f2.2 [A ~+> B,B ~+> B] f34.7 ~> f36.12 [] f8.3 ~> f34.7 [B ~=> D] f27.16 ~> f34.7 [] f19.11 ~> f27.16 [] f8.9 ~> f19.11 [] f8.4 ~> f8.9 [E ~=> D,huge ~=> C,E ~+> E,K ~+> E] f2.2 ~> f8.4 [B ~=> D,K ~=> C] f8.4 ~> f8.4 [E ~=> D,huge ~=> C,E ~+> E,K ~+> E] f8.5 ~> f8.4 [E ~+> E,K ~+> E] f8.4 ~> f8.5 [E ~=> D,huge ~=> C,E ~+> E,K ~+> E] f8.5 ~> f8.5 [E ~+> E,K ~+> E] f8.5 ~> f8.9 [E ~+> E,K ~+> E] f8.10 ~> f19.11 [] f8.5 ~> f8.10 [E ~+> E,K ~+> E] f34.8 ~> f36.12 [] f8.3 ~> f34.8 [B ~=> D] f27.16 ~> f34.8 [] f36.13 ~> f36.12 [D ~+> D,E ~+> D] f34.7 ~> f36.13 [] f34.8 ~> f36.13 [] f36.13 ~> f36.13 [D ~+> D,E ~+> D] f49.18 ~> f36.13 [D ~+> D,E ~+> D] f43.17 ~> f49.18 [] f36.14 ~> f43.17 [] f34.7 ~> f36.14 [] f34.8 ~> f36.14 [] f36.13 ~> f36.14 [D ~+> D,E ~+> D] f49.18 ~> f36.14 [D ~+> D,E ~+> D] f36.15 ~> f43.17 [] f34.7 ~> f36.15 [] f34.8 ~> f36.15 [] f36.13 ~> f36.15 [D ~+> D,E ~+> D] f49.18 ~> f36.15 [D ~+> D,E ~+> D] f49.18 ~> f36.12 [D ~+> D,E ~+> D] f27.16 ~> f34.6 [] + Loop: [A ~+> 0.0.0,D ~+> 0.0.0,K ~+> 0.0.0] f36.13 ~> f36.13 [D ~+> D,E ~+> D] f49.18 ~> f36.13 [D ~+> D,E ~+> D] f43.17 ~> f49.18 [] f36.14 ~> f43.17 [] f36.13 ~> f36.14 [D ~+> D,E ~+> D] f49.18 ~> f36.14 [D ~+> D,E ~+> D] f36.15 ~> f43.17 [] f36.13 ~> f36.15 [D ~+> D,E ~+> D] f49.18 ~> f36.15 [D ~+> D,E ~+> D] + Applied Processor: Lare + Details: start.0 ~> exitus616.20 [B ~=> D ,E ~=> D ,K ~=> C ,huge ~=> C ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> B ,E ~+> D ,E ~+> E ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,E ~*> B ,E ~*> D ,E ~*> E ,E ~*> 0.0.0 ,E ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,E ~^> D ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + f34.6> [B ~=> D ,E ~=> D ,K ~=> C ,huge ~=> C ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> B ,E ~+> D ,E ~+> E ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,E ~*> B ,E ~*> D ,E ~*> E ,E ~*> 0.0.0 ,E ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,E ~^> D ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] f36.12> [B ~=> D ,E ~=> D ,K ~=> C ,huge ~=> C ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> B ,E ~+> D ,E ~+> E ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,E ~*> B ,E ~*> D ,E ~*> E ,E ~*> 0.0.0 ,E ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,E ~^> D ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + f36.13> [A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f49.18> [A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f36.13> [A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f49.18> [A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f36.13> [A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f49.18> [A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] YES(?,PRIMREC)