YES * Step 1: FromIts YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f12(H,I,J,0,E,F,G) True (1,1) 1. f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [D >= 0 && C >= 1 + D] (?,1) 2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1) 3. f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] (?,1) 4. f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H) [D >= 0 && D >= C] (?,1) Signature: {(f0,7);(f12,7);(f25,7);(f34,7)} Flow Graph: [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: f0(A,B,C,D,E,F,G) -> f12(H,I,J,0,E,F,G) True f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [D >= 0 && C >= 1 + D] f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H) [D >= 0 && D >= C] Signature: {(f0,7);(f12,7);(f25,7);(f34,7)} Rule Graph: [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4] | +- p:[1] c: [1] | `- p:[2] c: [2] * Step 3: CloseWith YES + Considered Problem: (Rules: f0(A,B,C,D,E,F,G) -> f12(H,I,J,0,E,F,G) True f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [D >= 0 && C >= 1 + D] f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H) [D >= 0 && D >= C] Signature: {(f0,7);(f12,7);(f25,7);(f34,7)} Rule Graph: [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}] ,We construct a looptree: P: [0,1,2,3,4] | +- p:[1] c: [1] | `- p:[2] c: [2]) + Applied Processor: CloseWith True + Details: () YES