YES * Step 1: FromIts YES + 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: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Rule 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: Decompose NoGreedy + 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] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [11,17] | `- p:[3,12,5,14,7,15,9,16,13] c: [9,16] | `- p:[3,12,5,14,7,15,13] c: [7,15] | `- p:[3,12,5,14,13] c: [5,14] | `- p:[3,12,13] c: [13] | `- p:[3,12] c: [3,12] * Step 3: CloseWith YES + Considered Problem: (Rules: 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Rule 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}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [11,17] | `- p:[3,12,5,14,7,15,9,16,13] c: [9,16] | `- p:[3,12,5,14,7,15,13] c: [7,15] | `- p:[3,12,5,14,13] c: [5,14] | `- p:[3,12,13] c: [13] | `- p:[3,12] c: [3,12]) + Applied Processor: CloseWith True + Details: () YES