YES * Step 1: UnsatRules YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1) 1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1) 2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1) 3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 6. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [2 >= H && 9 >= B && B >= 0 && H >= A && H >= 3 && 4 >= H && F = 1 + B] (?,1) 7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1) 8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1) 9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1) Signature: {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{3,4,5},2->{6,7,8},3->{},4->{3,4,5},5->{6,7,8},6->{3,4,5},7->{3,4,5},8->{6,7,8},9->{0,1,2}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [6] * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1) 1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1) 2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1) 3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1) 8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1) 9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1) Signature: {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{3,4,5},2->{7,8},3->{},4->{3,4,5},5->{7,8},7->{3,4,5},8->{7,8},9->{0,1,2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3),(2,7),(4,3),(5,7),(7,4)] * Step 3: FromIts YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1) 1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1) 2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1) 3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1) 7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1) 8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1) 9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1) Signature: {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{4,5},2->{8},3->{},4->{4,5},5->{8},7->{3,5},8->{7,8},9->{0,1,2}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True Signature: {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)} Rule Graph: [0->{},1->{4,5},2->{8},3->{},4->{4,5},5->{8},7->{3,5},8->{7,8},9->{0,1,2}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,7,8,9] | +- p:[4] c: [4] | `- p:[5,7,8] c: [5,7,8] * Step 5: CloseWith YES + Considered Problem: (Rules: start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True Signature: {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)} Rule Graph: [0->{},1->{4,5},2->{8},3->{},4->{4,5},5->{8},7->{3,5},8->{7,8},9->{0,1,2}] ,We construct a looptree: P: [0,1,2,3,4,5,7,8,9] | +- p:[4] c: [4] | `- p:[5,7,8] c: [5,7,8]) + Applied Processor: CloseWith True + Details: () YES