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) [B >= 1 && D >= 0 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] (?,1) 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 (?,1) && D >= 0 && 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) [B >= 1 && D >= 0 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] (?,1) 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] (?,1) 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) [B >= 1 && D >= 0 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] (?,1) 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 (?,1) && D >= 0 && 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) [B >= 1 && D >= 0 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] (?,1) 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] (?,1) 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 + x5 p(start) = 1 + -1*x1 + x5 Following rules are strictly oriented: [B >= 1 && D >= 0 && 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 + E > 1 + E + -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 + E >= 1 + -1*A + E = m1(A,B,C,D,E,F) [B >= 1 && D >= 0 && 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 + E >= 1 + -1*A + E = m1(A,B,H,D,E,G) [B >= 1 ==> && D >= 0 && 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 + E >= 1 + E + -1*H = m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && 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 + E >= 1 + -1*A + E = 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) [B >= 1 && D >= 0 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] (?,1) 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 (?,1) && D >= 0 && 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) [B >= 1 && D >= 0 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] (?,1) 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] (1 + A + E,1) 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: [B >= 1 && D >= 0 && 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) [B >= 1 && D >= 0 && 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) [B >= 1 ==> && D >= 0 && 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) [B >= 1 && D >= 0 && 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) [B >= 1 && D >= 0 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] (?,1) 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 (?,1) && D >= 0 && 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) [B >= 1 && D >= 0 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] (1 + B + C,1) 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] (1 + A + E,1) 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 + x5 p(start) = 1 + -1*x1 + x5 Following rules are strictly oriented: [B >= 1 ==> && D >= 0 && 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 + E > 1 + E + -1*H = m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && 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 + E > 1 + E + -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 + E >= 1 + -1*A + E = m1(A,B,C,D,E,F) [B >= 1 && D >= 0 && 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 + E >= 1 + -1*A + E = m1(A,B,H,D,E,G) [B >= 1 && D >= 0 && 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 + E >= 1 + -1*A + E = 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) [B >= 1 && D >= 0 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] (?,1) 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 (1 + A + E,1) && D >= 0 && 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) [B >= 1 && D >= 0 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] (1 + B + C,1) 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] (1 + A + E,1) 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: [B >= 1 && D >= 0 && 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) [B >= 1 ==> && D >= 0 && 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) [B >= 1 && D >= 0 && 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) [B >= 1 && D >= 0 && 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) [B >= 1 && D >= 0 && A >= 1 + E && 1 + B >= G && 1 + C >= H && H >= 1 + C && 1 + F >= G && G >= 1 + F] (1 + B + F,1) 2. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 (1 + A + E,1) && D >= 0 && 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) [B >= 1 && D >= 0 && B >= F && 1 + B >= H && E >= A && 1 + F >= G && G >= 1 + F && 1 + C >= H && H >= 1 + C] (1 + B + C,1) 4. m1(A,B,C,D,E,F) -> m1(H,B,C,D,E,G) [B >= 1 && D >= 0 && B >= F && B >= C && 1 + E >= H && 1 + A >= H && H >= 1 + A && 1 + F >= G && G >= 1 + F] (1 + A + E,1) 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))