YES(?,O(n^1)) * Step 1: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> m1(A,B,C,D,E,F) [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] (1,1) 1. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] 3. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] Signature: {(m1,6);(start,6)} Flow Graph: [0->{1,2,3,4},1->{1,2,3,4},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,1),(0,2),(1,2),(1,3),(1,4),(2,3),(2,4),(3,1),(4,2)] * Step 2: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> m1(A,B,C,D,E,F) [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] (1,1) 1. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] 3. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] Signature: {(m1,6);(start,6)} Flow Graph: [0->{3,4},1->{1},2->{1,2},3->{2,3,4},4->{1,3,4}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(m1) = 1 + -1*x1 + x2 p(start) = 1 + -1*x1 + x2 Following rules are strictly oriented: [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + -1*A + B > 1 + B + -1*H = m1(H,B,C,D,E,G) Following rules are weakly oriented: [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] ==> start(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + -1*A + B = m1(A,B,C,D,E,F) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + -1*A + B = m1(A,B,H,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] m1(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + B + -1*H = m1(H,B,C,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] m1(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + -1*A + B = m1(A,B,H,D,E,G) * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> m1(A,B,C,D,E,F) [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] (1,1) 1. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] 3. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (1 + A + B,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] Signature: {(m1,6);(start,6)} Flow Graph: [0->{3,4},1->{1},2->{1,2},3->{2,3,4},4->{1,3,4}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(m1) = 1 + x2 + -1*x3 p(start) = 1 + x2 + -1*x3 Following rules are strictly oriented: [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] m1(A,B,C,D,E,F) = 1 + B + -1*C > 1 + B + -1*H = m1(A,B,H,D,E,G) Following rules are weakly oriented: [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] ==> start(A,B,C,D,E,F) = 1 + B + -1*C >= 1 + B + -1*C = m1(A,B,C,D,E,F) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + B + -1*C >= 1 + B + -1*H = m1(A,B,H,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] m1(A,B,C,D,E,F) = 1 + B + -1*C >= 1 + B + -1*C = m1(H,B,C,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + B + -1*C >= 1 + B + -1*C = m1(H,B,C,D,E,G) * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> m1(A,B,C,D,E,F) [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] (1,1) 1. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] 3. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (1 + B + C,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (1 + A + B,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] Signature: {(m1,6);(start,6)} Flow Graph: [0->{3,4},1->{1},2->{1,2},3->{2,3,4},4->{1,3,4}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(m1) = 1 + -1*x1 + x2 p(start) = 1 + -1*x1 + x2 Following rules are strictly oriented: [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] m1(A,B,C,D,E,F) = 1 + -1*A + B > 1 + B + -1*H = m1(H,B,C,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + -1*A + B > 1 + B + -1*H = m1(H,B,C,D,E,G) Following rules are weakly oriented: [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] ==> start(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + -1*A + B = m1(A,B,C,D,E,F) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + -1*A + B = m1(A,B,H,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] m1(A,B,C,D,E,F) = 1 + -1*A + B >= 1 + -1*A + B = m1(A,B,H,D,E,G) * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> m1(A,B,C,D,E,F) [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] (1,1) 1. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (?,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (1 + A + B,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] 3. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (1 + B + C,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (1 + A + B,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] Signature: {(m1,6);(start,6)} Flow Graph: [0->{3,4},1->{1},2->{1,2},3->{2,3,4},4->{1,3,4}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(m1) = 1 + x2 + -1*x6 p(start) = 1 + x2 + -1*x6 Following rules are strictly oriented: [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + B + -1*F > 1 + B + -1*G = m1(A,B,H,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] m1(A,B,C,D,E,F) = 1 + B + -1*F > 1 + B + -1*G = m1(H,B,C,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] m1(A,B,C,D,E,F) = 1 + B + -1*F > 1 + B + -1*G = m1(A,B,H,D,E,G) [F >= 0 ==> && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] m1(A,B,C,D,E,F) = 1 + B + -1*F > 1 + B + -1*G = m1(H,B,C,D,E,G) Following rules are weakly oriented: [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] ==> start(A,B,C,D,E,F) = 1 + B + -1*F >= 1 + B + -1*F = m1(A,B,C,D,E,F) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> m1(A,B,C,D,E,F) [A >= 0 && 2 + A + B >= 2*C && B >= 1 + A && 2*C >= A + B && D >= 0 && 1 + E = C && F = A] (1,1) 1. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (1 + B + F,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (1 + A + B,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + E >= H && C >= 1 + B && 1 + F >= G && G >= 1 + F && 1 + A >= H && H >= 1 + A] 3. m1(A,B,C,D,E,F) -> m1(A,B,H,D,E,G) [F >= 0 (1 + B + C,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [F >= 0 (1 + A + B,1) && E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -1 + C + -1*E >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && B >= 1 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] Signature: {(m1,6);(start,6)} Flow Graph: [0->{3,4},1->{1},2->{1,2},3->{2,3,4},4->{1,3,4}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))