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