YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f52(5,14,0,0,E,F,G) True (1,1) 1. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + C,E,F,G) [A >= 1 + D && C = D] (?,1) 2. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && C >= 1 + D] (?,1) 3. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && D >= 1 + C] (?,1) 4. f60(A,B,C,D,E,F,G) -> f63(A,B,C,D,0,F,G) [A >= 1 + D] (?,1) 5. f63(A,B,C,D,E,F,G) -> f63(A,B,C,D,1 + E,H,I) [B >= 1 + E] (?,1) 6. f74(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,H,I) [B >= 1 + D] (?,1) 7. f74(A,B,C,D,E,F,G) -> f74(A,B,C,1 + D,E,H,I) [B >= 1 + D] (?,1) 8. f84(A,B,C,D,E,F,G) -> f84(A,B,C,1 + D,E,F,G) [A >= 1 + D] (?,1) 9. f84(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,F,G) [D >= A] (?,1) 10. f74(A,B,C,D,E,F,G) -> f84(A,B,C,0,E,F,G) [D >= B] (?,1) 11. f63(A,B,C,D,E,F,G) -> f60(A,B,C,1 + D,E,F,G) [E >= B] (?,1) 12. f60(A,B,C,D,E,F,G) -> f74(A,B,C,0,E,F,G) [D >= A] (?,1) 13. f52(A,B,C,D,E,F,G) -> f60(A,B,C,0,E,F,G) [D >= A] (?,1) Signature: {(f0,7);(f52,7);(f60,7);(f63,7);(f74,7);(f80,7);(f84,7)} Flow Graph: [0->{1,2,3,13},1->{1,2,3,13},2->{1,2,3,13},3->{1,2,3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9} ,9->{},10->{8,9},11->{4,12},12->{6,7,10},13->{4,12}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2),(0,3),(0,13),(1,1),(1,2),(2,3),(3,1),(3,2)] * Step 2: UnreachableRules YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f52(5,14,0,0,E,F,G) True (1,1) 1. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + C,E,F,G) [A >= 1 + D && C = D] (?,1) 2. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && C >= 1 + D] (?,1) 3. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && D >= 1 + C] (?,1) 4. f60(A,B,C,D,E,F,G) -> f63(A,B,C,D,0,F,G) [A >= 1 + D] (?,1) 5. f63(A,B,C,D,E,F,G) -> f63(A,B,C,D,1 + E,H,I) [B >= 1 + E] (?,1) 6. f74(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,H,I) [B >= 1 + D] (?,1) 7. f74(A,B,C,D,E,F,G) -> f74(A,B,C,1 + D,E,H,I) [B >= 1 + D] (?,1) 8. f84(A,B,C,D,E,F,G) -> f84(A,B,C,1 + D,E,F,G) [A >= 1 + D] (?,1) 9. f84(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,F,G) [D >= A] (?,1) 10. f74(A,B,C,D,E,F,G) -> f84(A,B,C,0,E,F,G) [D >= B] (?,1) 11. f63(A,B,C,D,E,F,G) -> f60(A,B,C,1 + D,E,F,G) [E >= B] (?,1) 12. f60(A,B,C,D,E,F,G) -> f74(A,B,C,0,E,F,G) [D >= A] (?,1) 13. f52(A,B,C,D,E,F,G) -> f60(A,B,C,0,E,F,G) [D >= A] (?,1) Signature: {(f0,7);(f52,7);(f60,7);(f63,7);(f74,7);(f80,7);(f84,7)} Flow Graph: [0->{1},1->{3,13},2->{1,2,13},3->{3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9},9->{},10->{8,9} ,11->{4,12},12->{6,7,10},13->{4,12}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [2] * Step 3: FromIts YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f52(5,14,0,0,E,F,G) True (1,1) 1. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + C,E,F,G) [A >= 1 + D && C = D] (?,1) 3. f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && D >= 1 + C] (?,1) 4. f60(A,B,C,D,E,F,G) -> f63(A,B,C,D,0,F,G) [A >= 1 + D] (?,1) 5. f63(A,B,C,D,E,F,G) -> f63(A,B,C,D,1 + E,H,I) [B >= 1 + E] (?,1) 6. f74(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,H,I) [B >= 1 + D] (?,1) 7. f74(A,B,C,D,E,F,G) -> f74(A,B,C,1 + D,E,H,I) [B >= 1 + D] (?,1) 8. f84(A,B,C,D,E,F,G) -> f84(A,B,C,1 + D,E,F,G) [A >= 1 + D] (?,1) 9. f84(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,F,G) [D >= A] (?,1) 10. f74(A,B,C,D,E,F,G) -> f84(A,B,C,0,E,F,G) [D >= B] (?,1) 11. f63(A,B,C,D,E,F,G) -> f60(A,B,C,1 + D,E,F,G) [E >= B] (?,1) 12. f60(A,B,C,D,E,F,G) -> f74(A,B,C,0,E,F,G) [D >= A] (?,1) 13. f52(A,B,C,D,E,F,G) -> f60(A,B,C,0,E,F,G) [D >= A] (?,1) Signature: {(f0,7);(f52,7);(f60,7);(f63,7);(f74,7);(f80,7);(f84,7)} Flow Graph: [0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9},9->{},10->{8,9},11->{4,12} ,12->{6,7,10},13->{4,12}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: f0(A,B,C,D,E,F,G) -> f52(5,14,0,0,E,F,G) True f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + C,E,F,G) [A >= 1 + D && C = D] f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && D >= 1 + C] f60(A,B,C,D,E,F,G) -> f63(A,B,C,D,0,F,G) [A >= 1 + D] f63(A,B,C,D,E,F,G) -> f63(A,B,C,D,1 + E,H,I) [B >= 1 + E] f74(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,H,I) [B >= 1 + D] f74(A,B,C,D,E,F,G) -> f74(A,B,C,1 + D,E,H,I) [B >= 1 + D] f84(A,B,C,D,E,F,G) -> f84(A,B,C,1 + D,E,F,G) [A >= 1 + D] f84(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,F,G) [D >= A] f74(A,B,C,D,E,F,G) -> f84(A,B,C,0,E,F,G) [D >= B] f63(A,B,C,D,E,F,G) -> f60(A,B,C,1 + D,E,F,G) [E >= B] f60(A,B,C,D,E,F,G) -> f74(A,B,C,0,E,F,G) [D >= A] f52(A,B,C,D,E,F,G) -> f60(A,B,C,0,E,F,G) [D >= A] Signature: {(f0,7);(f52,7);(f60,7);(f63,7);(f74,7);(f80,7);(f84,7)} Rule Graph: [0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9},9->{},10->{8,9},11->{4,12} ,12->{6,7,10},13->{4,12}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,3,4,5,6,7,8,9,10,11,12,13] | +- p:[3] c: [3] | +- p:[4,11,5] c: [4,11] | | | `- p:[5] c: [5] | +- p:[7] c: [7] | `- p:[8] c: [8] * Step 5: CloseWith YES + Considered Problem: (Rules: f0(A,B,C,D,E,F,G) -> f52(5,14,0,0,E,F,G) True f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + C,E,F,G) [A >= 1 + D && C = D] f52(A,B,C,D,E,F,G) -> f52(A,B,C,1 + D,E,F,G) [A >= 1 + D && D >= 1 + C] f60(A,B,C,D,E,F,G) -> f63(A,B,C,D,0,F,G) [A >= 1 + D] f63(A,B,C,D,E,F,G) -> f63(A,B,C,D,1 + E,H,I) [B >= 1 + E] f74(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,H,I) [B >= 1 + D] f74(A,B,C,D,E,F,G) -> f74(A,B,C,1 + D,E,H,I) [B >= 1 + D] f84(A,B,C,D,E,F,G) -> f84(A,B,C,1 + D,E,F,G) [A >= 1 + D] f84(A,B,C,D,E,F,G) -> f80(A,B,C,D,E,F,G) [D >= A] f74(A,B,C,D,E,F,G) -> f84(A,B,C,0,E,F,G) [D >= B] f63(A,B,C,D,E,F,G) -> f60(A,B,C,1 + D,E,F,G) [E >= B] f60(A,B,C,D,E,F,G) -> f74(A,B,C,0,E,F,G) [D >= A] f52(A,B,C,D,E,F,G) -> f60(A,B,C,0,E,F,G) [D >= A] Signature: {(f0,7);(f52,7);(f60,7);(f63,7);(f74,7);(f80,7);(f84,7)} Rule Graph: [0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9},9->{},10->{8,9},11->{4,12} ,12->{6,7,10},13->{4,12}] ,We construct a looptree: P: [0,1,3,4,5,6,7,8,9,10,11,12,13] | +- p:[3] c: [3] | +- p:[4,11,5] c: [4,11] | | | `- p:[5] c: [5] | +- p:[7] c: [7] | `- p:[8] c: [8]) + Applied Processor: CloseWith True + Details: () YES