YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> a(A,B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1 && B = A && C = D && E = F && G = H] 1. a(A,B,C,D,E,F,G,H) -> d(A,B,1,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && G = H && E = F && C = D && B = A] 2. d(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + C,H) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 + C && A >= C && A >= 1 && C >= 1 && B = A] 3. d(A,B,C,D,E,F,G,H) -> halt(A,B,C,D,E,F,G,H) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && C = A && B = A] 4. b(A,B,C,D,E,F,G,H) -> d(A,B,1 + C,D,E,F,G,H) [1 + B + -1*G >= 0 (?,1) && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= 1 + C && C >= 1 && A >= C && G = 1 + A && B = A] 5. b(A,B,C,D,E,F,G,H) -> c(A,B,C,D,B,F,G,H) [1 + B + -1*G >= 0 (?,1) && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= G && 1 + A >= G && A >= 1 + C && C >= 1 && G >= 1 + C && B = A] 6. c(A,B,C,D,E,F,G,H) -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0 (?,1) && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && E >= 1 + C && A >= E && A >= G && C >= 1 && E >= C && G >= 1 + C && B = A] 7. c(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + G,H) [B + -1*G >= 0 (?,1) && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= E && A >= G && E >= 1 && G >= 1 + E && C = E && B = A] 8. start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H) True (1,1) Signature: {(a,8);(b,8);(c,8);(d,8);(halt,8);(start,8);(start0,8)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{},4->{2,3},5->{6,7},6->{6,7},7->{4,5},8->{0}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,4),(5,7)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> a(A,B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1 && B = A && C = D && E = F && G = H] 1. a(A,B,C,D,E,F,G,H) -> d(A,B,1,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && G = H && E = F && C = D && B = A] 2. d(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + C,H) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 + C && A >= C && A >= 1 && C >= 1 && B = A] 3. d(A,B,C,D,E,F,G,H) -> halt(A,B,C,D,E,F,G,H) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && C = A && B = A] 4. b(A,B,C,D,E,F,G,H) -> d(A,B,1 + C,D,E,F,G,H) [1 + B + -1*G >= 0 (?,1) && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= 1 + C && C >= 1 && A >= C && G = 1 + A && B = A] 5. b(A,B,C,D,E,F,G,H) -> c(A,B,C,D,B,F,G,H) [1 + B + -1*G >= 0 (?,1) && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= G && 1 + A >= G && A >= 1 + C && C >= 1 && G >= 1 + C && B = A] 6. c(A,B,C,D,E,F,G,H) -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0 (?,1) && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && E >= 1 + C && A >= E && A >= G && C >= 1 && E >= C && G >= 1 + C && B = A] 7. c(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + G,H) [B + -1*G >= 0 (?,1) && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= E && A >= G && E >= 1 && G >= 1 + E && C = E && B = A] 8. start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H) True (1,1) Signature: {(a,8);(b,8);(c,8);(d,8);(halt,8);(start,8);(start0,8)} Flow Graph: [0->{1},1->{2,3},2->{5},3->{},4->{2,3},5->{6},6->{6,7},7->{4,5},8->{0}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: start(A,B,C,D,E,F,G,H) -> a(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1 && B = A && C = D && E = F && G = H] a(A,B,C,D,E,F,G,H) -> d(A,B,1,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && G = H && E = F && C = D && B = A] d(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + C,H) [B + -1*C >= 0 && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 + C && A >= C && A >= 1 && C >= 1 && B = A] d(A,B,C,D,E,F,G,H) -> halt(A,B,C,D,E,F,G,H) [B + -1*C >= 0 && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && C = A && B = A] b(A,B,C,D,E,F,G,H) -> d(A,B,1 + C,D,E,F,G,H) [1 + B + -1*G >= 0 && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= 1 + C && C >= 1 && A >= C && G = 1 + A && B = A] b(A,B,C,D,E,F,G,H) -> c(A,B,C,D,B,F,G,H) [1 + B + -1*G >= 0 && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= G && 1 + A >= G && A >= 1 + C && C >= 1 && G >= 1 + C && B = A] c(A,B,C,D,E,F,G,H) -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0 && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && E >= 1 + C && A >= E && A >= G && C >= 1 && E >= C && G >= 1 + C && B = A] c(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + G,H) [B + -1*G >= 0 && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= E && A >= G && E >= 1 && G >= 1 + E && C = E && B = A] start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H) True Signature: {(a,8);(b,8);(c,8);(d,8);(halt,8);(start,8);(start0,8)} Rule Graph: [0->{1},1->{2,3},2->{5},3->{},4->{2,3},5->{6},6->{6,7},7->{4,5},8->{0}] + Applied Processor: AddSinks + Details: () * Step 4: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: start(A,B,C,D,E,F,G,H) -> a(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1 && B = A && C = D && E = F && G = H] a(A,B,C,D,E,F,G,H) -> d(A,B,1,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && G = H && E = F && C = D && B = A] d(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + C,H) [B + -1*C >= 0 && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 + C && A >= C && A >= 1 && C >= 1 && B = A] d(A,B,C,D,E,F,G,H) -> halt(A,B,C,D,E,F,G,H) [B + -1*C >= 0 && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && C = A && B = A] b(A,B,C,D,E,F,G,H) -> d(A,B,1 + C,D,E,F,G,H) [1 + B + -1*G >= 0 && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= 1 + C && C >= 1 && A >= C && G = 1 + A && B = A] b(A,B,C,D,E,F,G,H) -> c(A,B,C,D,B,F,G,H) [1 + B + -1*G >= 0 && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= G && 1 + A >= G && A >= 1 + C && C >= 1 && G >= 1 + C && B = A] c(A,B,C,D,E,F,G,H) -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0 && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && E >= 1 + C && A >= E && A >= G && C >= 1 && E >= C && G >= 1 + C && B = A] c(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + G,H) [B + -1*G >= 0 && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= E && A >= G && E >= 1 && G >= 1 + E && C = E && B = A] start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H) True halt(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(a,8);(b,8);(c,8);(d,8);(exitus616,8);(halt,8);(start,8);(start0,8)} Rule Graph: [0->{1},1->{2,3},2->{5},3->{9},4->{2,3},5->{6},6->{6,7},7->{4,5},8->{0}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[2,4,7,6,5] c: [2,4] | `- p:[5,7,6] c: [5,7] | `- p:[6] c: [6] * Step 5: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: start(A,B,C,D,E,F,G,H) -> a(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 1 && B = A && C = D && E = F && G = H] a(A,B,C,D,E,F,G,H) -> d(A,B,1,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && G = H && E = F && C = D && B = A] d(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + C,H) [B + -1*C >= 0 && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 + C && A >= C && A >= 1 && C >= 1 && B = A] d(A,B,C,D,E,F,G,H) -> halt(A,B,C,D,E,F,G,H) [B + -1*C >= 0 && A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && A >= 1 && C = A && B = A] b(A,B,C,D,E,F,G,H) -> d(A,B,1 + C,D,E,F,G,H) [1 + B + -1*G >= 0 && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= 1 + C && C >= 1 && A >= C && G = 1 + A && B = A] b(A,B,C,D,E,F,G,H) -> c(A,B,C,D,B,F,G,H) [1 + B + -1*G >= 0 && 1 + A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= G && 1 + A >= G && A >= 1 + C && C >= 1 && G >= 1 + C && B = A] c(A,B,C,D,E,F,G,H) -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0 && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && E >= 1 + C && A >= E && A >= G && C >= 1 && E >= C && G >= 1 + C && B = A] c(A,B,C,D,E,F,G,H) -> b(A,B,C,D,E,F,1 + G,H) [B + -1*G >= 0 && A + -1*G >= 0 && -2 + G >= 0 && -3 + C + G >= 0 && -1 + -1*C + G >= 0 && -4 + B + G >= 0 && -4 + A + G >= 0 && B + -1*E >= 0 && A + -1*E >= 0 && -1 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && -2 + A >= 0 && A >= E && A >= G && E >= 1 && G >= 1 + E && C = E && B = A] start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H) True halt(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(a,8);(b,8);(c,8);(d,8);(exitus616,8);(halt,8);(start,8);(start0,8)} Rule Graph: [0->{1},1->{2,3},2->{5},3->{9},4->{2,3},5->{6},6->{6,7},7->{4,5},8->{0}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[2,4,7,6,5] c: [2,4] | `- p:[5,7,6] c: [5,7] | `- p:[6] c: [6]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,0.0,0.0.0,0.0.0.0] start ~> a [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] a ~> d [A <= A, B <= B, C <= K, D <= D, E <= E, F <= F, G <= G, H <= H] d ~> b [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B, H <= H] d ~> halt [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] b ~> d [A <= A, B <= B, C <= B, D <= D, E <= E, F <= F, G <= G, H <= H] b ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c ~> b [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] start0 ~> start [A <= A, B <= A, C <= D, D <= D, E <= F, F <= F, G <= H, H <= H] halt ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0 <= A + C] d ~> b [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B, H <= H] b ~> d [A <= A, B <= B, C <= B, D <= D, E <= E, F <= F, G <= G, H <= H] c ~> b [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] c ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] b ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Loop: [0.0.0 <= A + G] b ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c ~> b [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] c ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Loop: [0.0.0.0 <= C + E] c ~> c [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,0.0,0.0.0,0.0.0.0] start ~> a [] a ~> d [K ~=> C] d ~> b [B ~=> G] d ~> halt [] b ~> d [B ~=> C] b ~> c [B ~=> E] c ~> c [B ~=> E] c ~> b [B ~+> G,G ~+> G] start0 ~> start [A ~=> B,D ~=> C,F ~=> E,H ~=> G] halt ~> exitus616 [] + Loop: [A ~+> 0.0,C ~+> 0.0] d ~> b [B ~=> G] b ~> d [B ~=> C] c ~> b [B ~+> G,G ~+> G] c ~> c [B ~=> E] b ~> c [B ~=> E] + Loop: [A ~+> 0.0.0,G ~+> 0.0.0] b ~> c [B ~=> E] c ~> b [B ~+> G,G ~+> G] c ~> c [B ~=> E] + Loop: [C ~+> 0.0.0.0,E ~+> 0.0.0.0] c ~> c [B ~=> E] + Applied Processor: Lare + Details: start0 ~> exitus616 [A ~=> B ,A ~=> C ,A ~=> E ,A ~=> G ,F ~=> E ,H ~=> G ,K ~=> C ,A ~+> G ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> G ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,K ~*> G ,K ~*> tick ,A ~^> G ,K ~^> G] + d> [B ~=> C ,B ~=> E ,B ~=> G ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> G ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> 0.0.0.0 ,C ~+> tick ,tick ~+> tick ,A ~*> G ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> G ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> tick ,C ~*> G ,C ~*> tick ,A ~^> G ,C ~^> G] + b> [B ~=> E ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> G ,B ~+> 0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0.0 ,C ~+> tick ,G ~+> G ,G ~+> 0.0.0 ,G ~+> tick ,tick ~+> tick ,A ~*> G ,A ~*> tick ,B ~*> G ,B ~*> tick ,C ~*> tick ,G ~*> G ,G ~*> tick] + c> [B ~=> E,C ~+> 0.0.0.0,C ~+> tick,E ~+> 0.0.0.0,E ~+> tick,tick ~+> tick] YES(?,POLY)