YES(?,O(n^1)) * Step 1: UnsatRules WORST_CASE(?,O(n^1)) + 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 WORST_CASE(?,O(n^1)) + 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: TrivialSCCs WORST_CASE(?,O(n^1)) + 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 4: PolyRank WORST_CASE(?,O(n^1)) + 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) 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,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,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,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl82) = 45 + -1*x2 + -9*x8 p(lbl92) = 36 + -9*x4 p(start) = 45 + -9*x1 p(start0) = 45 + -9*x1 p(stop) = 45 + -9*x8 Following rules are strictly oriented: [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==> lbl82(A,B,C,D,E,F,G,H) = 45 + -1*B + -9*H > 45 + -1*F + -9*H = lbl82(A,F,C,D,E,1 + F,G,H) Following rules are weakly oriented: [A >= 5 && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 45 + -9*A >= 45 + -9*H = stop(A,B,C,D,E,F,G,H) [2 >= A && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 45 + -9*A >= 36 + -9*H = lbl92(A,B,C,H,E,0,G,1 + H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 45 + -9*A >= 45 + -9*H = lbl82(A,0,C,D,E,1,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 36 + -9*D >= 45 + -9*H = stop(A,B,C,D,E,F,G,H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 36 + -9*D >= 36 + -9*H = lbl92(A,B,C,H,E,0,G,1 + H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 36 + -9*D >= 45 + -9*H = lbl82(A,0,C,D,E,1,G,H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==> lbl82(A,B,C,D,E,F,G,H) = 45 + -1*B + -9*H >= 36 + -9*H = lbl92(A,B,C,H,E,F,G,1 + H) True ==> start0(A,B,C,D,E,F,G,H) = 45 + -9*A >= 45 + -9*A = start(A,C,C,E,E,G,G,A) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + 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) 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,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,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,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] (45 + 9*A,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: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^1)) + 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) 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,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,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,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] (45 + 9*A,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] (45 + 9*A,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl82) = 4 + -1*x8 p(lbl92) = 4 + -1*x4 p(start) = 5 + -1*x1 p(start0) = 5 + -1*x1 p(stop) = 5 + -1*x8 Following rules are strictly oriented: [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 5 + -1*A > 4 + -1*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] ==> lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D > 4 + -1*H = lbl82(A,0,C,D,E,1,G,H) Following rules are weakly oriented: [A >= 5 && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 5 + -1*A >= 5 + -1*H = stop(A,B,C,D,E,F,G,H) [2 >= A && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 5 + -1*A >= 4 + -1*H = lbl92(A,B,C,H,E,0,G,1 + H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D >= 5 + -1*H = stop(A,B,C,D,E,F,G,H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D >= 4 + -1*H = lbl92(A,B,C,H,E,0,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==> lbl82(A,B,C,D,E,F,G,H) = 4 + -1*H >= 4 + -1*H = lbl92(A,B,C,H,E,F,G,1 + H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==> lbl82(A,B,C,D,E,F,G,H) = 4 + -1*H >= 4 + -1*H = lbl82(A,F,C,D,E,1 + F,G,H) True ==> start0(A,B,C,D,E,F,G,H) = 5 + -1*A >= 5 + -1*A = start(A,C,C,E,E,G,G,A) * Step 7: PolyRank WORST_CASE(?,O(n^1)) + 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) 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,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,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,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] (5 + A,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] (45 + 9*A,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] (45 + 9*A,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl82) = 36 + -8*x1 + -10*x8 p(lbl92) = 26 + -8*x1 + -10*x4 + x6 p(start) = 36 + -18*x1 p(start0) = 36 + -18*x1 p(stop) = 36 + -8*x1 + -10*x8 Following rules are strictly oriented: [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 26 + -8*A + -10*D + F > 26 + -8*A + -10*H = lbl92(A,B,C,H,E,0,G,1 + H) Following rules are weakly oriented: [A >= 5 && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 36 + -18*A >= 36 + -8*A + -10*H = stop(A,B,C,D,E,F,G,H) [2 >= A && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 36 + -18*A >= 26 + -8*A + -10*H = lbl92(A,B,C,H,E,0,G,1 + H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] ==> start(A,B,C,D,E,F,G,H) = 36 + -18*A >= 36 + -8*A + -10*H = lbl82(A,0,C,D,E,1,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 26 + -8*A + -10*D + F >= 36 + -8*A + -10*H = stop(A,B,C,D,E,F,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==> lbl92(A,B,C,D,E,F,G,H) = 26 + -8*A + -10*D + F >= 36 + -8*A + -10*H = lbl82(A,0,C,D,E,1,G,H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==> lbl82(A,B,C,D,E,F,G,H) = 36 + -8*A + -10*H >= 26 + -8*A + F + -10*H = lbl92(A,B,C,H,E,F,G,1 + H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==> lbl82(A,B,C,D,E,F,G,H) = 36 + -8*A + -10*H >= 36 + -8*A + -10*H = lbl82(A,F,C,D,E,1 + F,G,H) True ==> start0(A,B,C,D,E,F,G,H) = 36 + -18*A >= 36 + -18*A = start(A,C,C,E,E,G,G,A) * Step 8: KnowledgePropagation WORST_CASE(?,O(n^1)) + 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) 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,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,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,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] (36 + 18*A,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] (5 + A,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] (45 + 9*A,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] (45 + 9*A,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: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))