YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) 19. lbl191(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 20. lbl171(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 21. lbl141(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 22. lbl121(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 23. lbl21(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 24. start(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10) ;(lbl121,10) ;(lbl141,10) ;(lbl171,10) ;(lbl191,10) ;(lbl21,10) ;(lbl81,10) ;(start,10) ;(start0,10) ;(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3,23},13->{2,3,23},14->{4,5 ,22},15->{6,7,21},16->{8,9,20},17->{10,11,19},18->{0,1,24},19->{},20->{},21->{},22->{},23->{},24->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [17] | `- p:[3,12,5,14,7,15,9,16,13] c: [16] | `- p:[3,12,5,14,7,15,13] c: [15] | `- p:[3,12,5,14,13] c: [14] | `- p:[3,12,13] c: [13] | `- p:[3,12] c: [12] * Step 4: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) 19. lbl191(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 20. lbl171(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 21. lbl141(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 22. lbl121(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 23. lbl21(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) 24. start(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10) ;(lbl121,10) ;(lbl141,10) ;(lbl171,10) ;(lbl191,10) ;(lbl21,10) ;(lbl81,10) ;(start,10) ;(start0,10) ;(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3,23},13->{2,3,23},14->{4,5 ,22},15->{6,7,21},16->{8,9,20},17->{10,11,19},18->{0,1,24},19->{},20->{},21->{},22->{},23->{},24->{}] ,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] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [17] | `- p:[3,12,5,14,7,15,9,16,13] c: [16] | `- p:[3,12,5,14,7,15,13] c: [15] | `- p:[3,12,5,14,13] c: [14] | `- p:[3,12,13] c: [13] | `- p:[3,12] c: [12]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,0.0,0.0.0,0.0.0.0,0.0.0.0.0,0.0.0.0.0.0,0.0.0.0.0.0.0] start ~> stop [A <= A, B <= 0*K, C <= C, D <= 0*K, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= J] start ~> lbl81 [A <= A, B <= 0*K, C <= C, D <= 0*K, E <= E, F <= unknown, G <= G, H <= K, I <= I, J <= J] lbl21 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl121 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl141 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl171 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl171 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl191 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl191 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= B + J, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl141 [A <= A, B <= B, C <= C, D <= A + B, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl171 [A <= A, B <= A + D, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl191 [A <= A, B <= A + D, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] start0 ~> start [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= A] lbl191 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl171 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl21 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] start ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0 <= K + 3*A + H] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= B + J, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl141 [A <= A, B <= B, C <= C, D <= A + B, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl171 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl171 [A <= A, B <= A + D, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl191 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl191 [A <= A, B <= A + D, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0.0 <= K + A + H] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= B + J, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl141 [A <= A, B <= B, C <= C, D <= A + B, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl171 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl171 [A <= A, B <= A + D, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0.0.0 <= K + 2*A + B + D + H] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= B + J, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl141 [A <= A, B <= B, C <= C, D <= A + B, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0.0.0.0 <= K + A + H] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= B + J, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0.0.0.0.0 <= K + A + H] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0.0.0.0.0.0 <= K + A + H] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,0.0,0.0.0,0.0.0.0,0.0.0.0.0,0.0.0.0.0.0,0.0.0.0.0.0.0] start ~> stop [K ~=> B,K ~=> D,K ~=> H] start ~> lbl81 [K ~=> B,K ~=> D,K ~=> H,huge ~=> F] lbl21 ~> stop [] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl121 ~> stop [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl141 ~> stop [] lbl141 ~> lbl81 [J ~=> H,huge ~=> F] lbl171 ~> stop [] lbl171 ~> lbl81 [A ~=> H,huge ~=> F] lbl191 ~> stop [] lbl191 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl81 ~> lbl21 [] lbl81 ~> lbl121 [B ~+> D,J ~+> D] lbl81 ~> lbl141 [A ~+> D,B ~+> D] lbl81 ~> lbl171 [A ~+> B,D ~+> B] lbl81 ~> lbl191 [A ~+> B,D ~+> B] start0 ~> start [A ~=> J,C ~=> B,E ~=> D,G ~=> F,I ~=> H] lbl191 ~> exitus616 [] lbl171 ~> exitus616 [] lbl141 ~> exitus616 [] lbl121 ~> exitus616 [] lbl21 ~> exitus616 [] start ~> exitus616 [] + Loop: [H ~+> 0.0,K ~+> 0.0,A ~*> 0.0] lbl81 ~> lbl21 [] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl121 [B ~+> D,J ~+> D] lbl141 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl141 [A ~+> D,B ~+> D] lbl171 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl171 [A ~+> B,D ~+> B] lbl191 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl191 [A ~+> B,D ~+> B] + Loop: [A ~+> 0.0.0,H ~+> 0.0.0,K ~+> 0.0.0] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl121 [B ~+> D,J ~+> D] lbl141 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl141 [A ~+> D,B ~+> D] lbl171 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl171 [A ~+> B,D ~+> B] lbl81 ~> lbl21 [] + Loop: [B ~+> 0.0.0.0,D ~+> 0.0.0.0,H ~+> 0.0.0.0,K ~+> 0.0.0.0,A ~*> 0.0.0.0] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl121 [B ~+> D,J ~+> D] lbl141 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl141 [A ~+> D,B ~+> D] lbl81 ~> lbl21 [] + Loop: [A ~+> 0.0.0.0.0,H ~+> 0.0.0.0.0,K ~+> 0.0.0.0.0] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl121 [B ~+> D,J ~+> D] lbl81 ~> lbl21 [] + Loop: [A ~+> 0.0.0.0.0.0,H ~+> 0.0.0.0.0.0,K ~+> 0.0.0.0.0.0] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl81 ~> lbl21 [] + Loop: [A ~+> 0.0.0.0.0.0.0,H ~+> 0.0.0.0.0.0.0,K ~+> 0.0.0.0.0.0.0] lbl21 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] + Applied Processor: LareProcessor + Details: start0 ~> exitus616 [A ~=> H ,A ~=> J ,C ~=> B ,E ~=> D ,G ~=> F ,I ~=> H ,K ~=> B ,K ~=> D ,K ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.0.0.0.0 ,K ~*> tick] start0 ~> stop [A ~=> H ,A ~=> J ,G ~=> F ,K ~=> B ,K ~=> D ,K ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.0.0.0.0 ,K ~*> tick] + lbl21> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0 ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl141> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0 ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl191> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0 ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl171> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0 ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl121> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0 ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] + lbl121> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl171> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl81> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> tick ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> tick] lbl141> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] lbl21> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> B ,A ~+> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> B ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0 ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> B ,J ~+> D ,J ~+> 0.0.0.0 ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> 0.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> D ,H ~*> 0.0.0.0 ,H ~*> tick ,J ~*> B ,J ~*> D ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick] + lbl121> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> D ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> tick ,D ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] lbl81> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> D ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> tick ,D ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] lbl141> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> tick ,D ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] lbl21> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> 0.0.0.0 ,D ~+> tick ,H ~+> 0.0.0.0 ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> D ,J ~+> 0.0.0.0.0 ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,B ~*> tick ,D ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] + lbl121> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> D ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] lbl81> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> D ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] lbl21> [A ~=> H ,J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> D ,H ~+> 0.0.0.0.0 ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> D ,J ~+> 0.0.0.0.0.0 ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.0.0.0.0.0.0 ,A ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] + lbl81> [J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,H ~*> tick ,K ~*> tick] lbl21> [J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,H ~+> 0.0.0.0.0.0 ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,J ~+> 0.0.0.0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,H ~*> tick ,J ~*> tick ,K ~*> tick] + lbl81> [J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick] lbl21> [J ~=> H ,huge ~=> F ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,H ~+> 0.0.0.0.0.0.0 ,H ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick] YES(?,POLY)