YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1) 6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1) 7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (?,1) 9. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1) 10. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1) 12. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{3,4,8},1->{10,12},2->{},3->{10,12},4->{10,12},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{3,4 ,8},11->{3,4,8},12->{3,4,8}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,10),(4,12),(10,3)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1) 6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1) 7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (?,1) 9. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1) 10. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1) 12. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{3,4,8},1->{10,12},2->{},3->{12},4->{10},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{4,8},11->{3 ,4,8},12->{3,4,8}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Rule Graph: [0->{3,4,8},1->{10,12},2->{},3->{12},4->{10},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{4,8},11->{3 ,4,8},12->{3,4,8}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[3,12] c: [3,12] | `- p:[4,10] c: [4,10] * Step 4: CloseWith YES + Considered Problem: (Rules: f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Rule Graph: [0->{3,4,8},1->{10,12},2->{},3->{12},4->{10},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{4,8},11->{3 ,4,8},12->{3,4,8}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[3,12] c: [3,12] | `- p:[4,10] c: [4,10]) + Applied Processor: CloseWith True + Details: () YES