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