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: Unfold 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: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H) -> a.1(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.1(A,B,C,D,E,F,G,H) -> d.2(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] a.1(A,B,C,D,E,F,G,H) -> d.3(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.2(A,B,C,D,E,F,G,H) -> b.5(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.3(A,B,C,D,E,F,G,H) -> halt.9(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.4(A,B,C,D,E,F,G,H) -> d.2(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.4(A,B,C,D,E,F,G,H) -> d.3(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.5(A,B,C,D,E,F,G,H) -> c.6(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.6(A,B,C,D,E,F,G,H) -> c.6(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.6(A,B,C,D,E,F,G,H) -> c.7(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.7(A,B,C,D,E,F,G,H) -> b.4(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] c.7(A,B,C,D,E,F,G,H) -> b.5(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.8(A,B,C,D,E,F,G,H) -> start.0(A,A,D,D,F,F,H,H) True Signature: {(a.1,8);(b.4,8);(b.5,8);(c.6,8);(c.7,8);(d.2,8);(d.3,8);(halt.9,8);(start.0,8);(start0.8,8)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{7},4->{},5->{3},6->{4},7->{8,9},8->{8,9},9->{10,11},10->{5,6},11->{7},12->{0}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H) -> a.1(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.1(A,B,C,D,E,F,G,H) -> d.2(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] a.1(A,B,C,D,E,F,G,H) -> d.3(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.2(A,B,C,D,E,F,G,H) -> b.5(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.3(A,B,C,D,E,F,G,H) -> halt.9(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.4(A,B,C,D,E,F,G,H) -> d.2(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.4(A,B,C,D,E,F,G,H) -> d.3(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.5(A,B,C,D,E,F,G,H) -> c.6(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.6(A,B,C,D,E,F,G,H) -> c.6(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.6(A,B,C,D,E,F,G,H) -> c.7(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.7(A,B,C,D,E,F,G,H) -> b.4(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] c.7(A,B,C,D,E,F,G,H) -> b.5(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.8(A,B,C,D,E,F,G,H) -> start.0(A,A,D,D,F,F,H,H) True halt.9(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True halt.9(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(a.1,8) ;(b.4,8) ;(b.5,8) ;(c.6,8) ;(c.7,8) ;(d.2,8) ;(d.3,8) ;(exitus616,8) ;(halt.9,8) ;(start.0,8) ;(start0.8,8)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{7},4->{13,14},5->{3},6->{4},7->{8,9},8->{8,9},9->{10,11},10->{5,6},11->{7} ,12->{0}] + 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] | `- p:[3,5,10,9,7,11,8] c: [3,5,10] | `- p:[7,11,9,8] c: [7,9,11] | `- p:[8] c: [8] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: start.0(A,B,C,D,E,F,G,H) -> a.1(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.1(A,B,C,D,E,F,G,H) -> d.2(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] a.1(A,B,C,D,E,F,G,H) -> d.3(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.2(A,B,C,D,E,F,G,H) -> b.5(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.3(A,B,C,D,E,F,G,H) -> halt.9(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.4(A,B,C,D,E,F,G,H) -> d.2(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.4(A,B,C,D,E,F,G,H) -> d.3(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.5(A,B,C,D,E,F,G,H) -> c.6(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.6(A,B,C,D,E,F,G,H) -> c.6(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.6(A,B,C,D,E,F,G,H) -> c.7(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.7(A,B,C,D,E,F,G,H) -> b.4(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] c.7(A,B,C,D,E,F,G,H) -> b.5(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.8(A,B,C,D,E,F,G,H) -> start.0(A,A,D,D,F,F,H,H) True halt.9(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True halt.9(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(a.1,8) ;(b.4,8) ;(b.5,8) ;(c.6,8) ;(c.7,8) ;(d.2,8) ;(d.3,8) ;(exitus616,8) ;(halt.9,8) ;(start.0,8) ;(start0.8,8)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{7},4->{13,14},5->{3},6->{4},7->{8,9},8->{8,9},9->{10,11},10->{5,6},11->{7} ,12->{0}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | `- p:[3,5,10,9,7,11,8] c: [3,5,10] | `- p:[7,11,9,8] c: [7,9,11] | `- p:[8] c: [8]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: 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.0 ~> a.1 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] a.1 ~> d.2 [A <= A, B <= B, C <= K, D <= D, E <= E, F <= F, G <= G, H <= H] a.1 ~> d.3 [A <= A, B <= B, C <= K, D <= D, E <= E, F <= F, G <= G, H <= H] d.2 ~> b.5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B, H <= H] d.3 ~> halt.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] b.4 ~> d.2 [A <= A, B <= B, C <= B, D <= D, E <= E, F <= F, G <= G, H <= H] b.4 ~> d.3 [A <= A, B <= B, C <= B, D <= D, E <= E, F <= F, G <= G, H <= H] b.5 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c.6 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c.6 ~> c.7 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c.7 ~> b.4 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] c.7 ~> b.5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] start0.8 ~> start.0 [A <= A, B <= A, C <= D, D <= D, E <= F, F <= F, G <= H, H <= H] halt.9 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] halt.9 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0 <= K + A + C] d.2 ~> b.5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B, H <= H] b.4 ~> d.2 [A <= A, B <= B, C <= B, D <= D, E <= E, F <= F, G <= G, H <= H] c.7 ~> b.4 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] c.6 ~> c.7 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] b.5 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c.7 ~> b.5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] c.6 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Loop: [0.0.0 <= A + G] b.5 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c.7 ~> b.5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= B + G, H <= H] c.6 ~> c.7 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] c.6 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Loop: [0.0.0.0 <= C + E] c.6 ~> c.6 [A <= A, B <= B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Applied Processor: AbstractFlow + Details: () * Step 8: 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.0 ~> a.1 [] a.1 ~> d.2 [K ~=> C] a.1 ~> d.3 [K ~=> C] d.2 ~> b.5 [B ~=> G] d.3 ~> halt.9 [] b.4 ~> d.2 [B ~=> C] b.4 ~> d.3 [B ~=> C] b.5 ~> c.6 [B ~=> E] c.6 ~> c.6 [B ~=> E] c.6 ~> c.7 [B ~=> E] c.7 ~> b.4 [B ~+> G,G ~+> G] c.7 ~> b.5 [B ~+> G,G ~+> G] start0.8 ~> start.0 [A ~=> B,D ~=> C,F ~=> E,H ~=> G] halt.9 ~> exitus616 [] halt.9 ~> exitus616 [] + Loop: [A ~+> 0.0,C ~+> 0.0,K ~+> 0.0] d.2 ~> b.5 [B ~=> G] b.4 ~> d.2 [B ~=> C] c.7 ~> b.4 [B ~+> G,G ~+> G] c.6 ~> c.7 [B ~=> E] b.5 ~> c.6 [B ~=> E] c.7 ~> b.5 [B ~+> G,G ~+> G] c.6 ~> c.6 [B ~=> E] + Loop: [A ~+> 0.0.0,G ~+> 0.0.0] b.5 ~> c.6 [B ~=> E] c.7 ~> b.5 [B ~+> G,G ~+> G] c.6 ~> c.7 [B ~=> E] c.6 ~> c.6 [B ~=> E] + Loop: [C ~+> 0.0.0.0,E ~+> 0.0.0.0] c.6 ~> c.6 [B ~=> E] + Applied Processor: Lare + Details: start0.8 ~> exitus616 [A ~=> B ,A ~=> C ,A ~=> E ,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 ~*> 0.0 ,K ~*> tick] + b.4> [B ~=> C ,B ~=> E ,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 ,K ~+> 0.0 ,K ~+> tick ,A ~*> G ,A ~*> tick ,B ~*> G ,B ~*> 0.0.0.0 ,B ~*> tick ,C ~*> tick ,K ~*> tick] + c.7> [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.6> [B ~=> E,C ~+> 0.0.0.0,C ~+> tick,E ~+> 0.0.0.0,E ~+> tick,tick ~+> tick] YES(?,POLY)