YES * Step 1: UnsatPaths YES + 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: Looptree YES + 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: Looptree + Details: We construct a looptree: P: [0,1,2,3,4] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | +- p:[2] c: [2] | `- p:[1] c: [1] YES