NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f26(A,B) -> f2(A,B) True (?,1) 1. f2(A,B) -> f2(A,B) True (?,1) 2. f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] (?,1) 3. f9(A,B) -> f12(A,C) [5 >= A && C >= 1] (?,1) 4. f12(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 5. f28(A,B) -> f30(A,B) True (?,1) 6. f20(A,B) -> f20(-1 + A,B) [A >= 3] (?,1) 7. f20(A,B) -> f9(A,B) [2 >= A] (?,1) 8. f12(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 9. f9(A,B) -> f20(A,0) [5 >= A] (?,1) 10. f9(A,B) -> f20(A,B) [A >= 6] (?,1) 11. f0(A,B) -> f9(C,B) True (1,1) Signature: {(f0,2);(f12,2);(f2,2);(f20,2);(f26,2);(f28,2);(f30,2);(f9,2)} Flow Graph: [0->{1},1->{1},2->{4,8},3->{4,8},4->{2,3,9,10},5->{},6->{6,7},7->{2,3,9,10},8->{2,3,9,10},9->{6,7},10->{6 ,7},11->{2,3,9,10}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,4),(3,4),(4,2),(4,3),(4,9),(7,10),(10,7)] * Step 2: UnreachableRules NO + Considered Problem: Rules: 0. f26(A,B) -> f2(A,B) True (?,1) 1. f2(A,B) -> f2(A,B) True (?,1) 2. f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] (?,1) 3. f9(A,B) -> f12(A,C) [5 >= A && C >= 1] (?,1) 4. f12(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 5. f28(A,B) -> f30(A,B) True (?,1) 6. f20(A,B) -> f20(-1 + A,B) [A >= 3] (?,1) 7. f20(A,B) -> f9(A,B) [2 >= A] (?,1) 8. f12(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 9. f9(A,B) -> f20(A,0) [5 >= A] (?,1) 10. f9(A,B) -> f20(A,B) [A >= 6] (?,1) 11. f0(A,B) -> f9(C,B) True (1,1) Signature: {(f0,2);(f12,2);(f2,2);(f20,2);(f26,2);(f28,2);(f30,2);(f9,2)} Flow Graph: [0->{1},1->{1},2->{8},3->{8},4->{10},5->{},6->{6,7},7->{2,3,9},8->{2,3,9,10},9->{6,7},10->{6},11->{2,3,9 ,10}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0,1,4,5] * Step 3: FromIts NO + Considered Problem: Rules: 2. f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] (?,1) 3. f9(A,B) -> f12(A,C) [5 >= A && C >= 1] (?,1) 6. f20(A,B) -> f20(-1 + A,B) [A >= 3] (?,1) 7. f20(A,B) -> f9(A,B) [2 >= A] (?,1) 8. f12(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 9. f9(A,B) -> f20(A,0) [5 >= A] (?,1) 10. f9(A,B) -> f20(A,B) [A >= 6] (?,1) 11. f0(A,B) -> f9(C,B) True (1,1) Signature: {(f0,2);(f12,2);(f2,2);(f20,2);(f26,2);(f28,2);(f30,2);(f9,2)} Flow Graph: [2->{8},3->{8},6->{6,7},7->{2,3,9},8->{2,3,9,10},9->{6,7},10->{6},11->{2,3,9,10}] + Applied Processor: FromIts + Details: () * Step 4: CloseWith NO + Considered Problem: Rules: f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] f9(A,B) -> f12(A,C) [5 >= A && C >= 1] f20(A,B) -> f20(-1 + A,B) [A >= 3] f20(A,B) -> f9(A,B) [2 >= A] f12(A,B) -> f9(1 + A,B) [5 >= A] f9(A,B) -> f20(A,0) [5 >= A] f9(A,B) -> f20(A,B) [A >= 6] f0(A,B) -> f9(C,B) True Signature: {(f0,2);(f12,2);(f2,2);(f20,2);(f26,2);(f28,2);(f30,2);(f9,2)} Rule Graph: [2->{8},3->{8},6->{6,7},7->{2,3,9},8->{2,3,9,10},9->{6,7},10->{6},11->{2,3,9,10}] + Applied Processor: CloseWith False + Details: () NO