MAYBE * Step 1: UnreachableRules MAYBE + 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: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0,1,5] * Step 2: UnsatPaths MAYBE + 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) 4. f12(A,B) -> f9(1 + A,B) [A >= 6] (?,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->{4,8},3->{4,8},4->{2,3,9,10},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 3: FromIts MAYBE + 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) 4. f12(A,B) -> f9(1 + A,B) [A >= 6] (?,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},4->{10},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: Unfold MAYBE + Considered Problem: Rules: f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] f9(A,B) -> f12(A,C) [5 >= A && C >= 1] f12(A,B) -> f9(1 + A,B) [A >= 6] 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},4->{10},6->{6,7},7->{2,3,9},8->{2,3,9,10},9->{6,7},10->{6},11->{2,3,9,10}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f9.2(A,B) -> f12.8(A,C) [5 >= A && 0 >= 1 + C] f9.3(A,B) -> f12.8(A,C) [5 >= A && C >= 1] f12.4(A,B) -> f9.10(1 + A,B) [A >= 6] f20.6(A,B) -> f20.6(-1 + A,B) [A >= 3] f20.6(A,B) -> f20.7(-1 + A,B) [A >= 3] f20.7(A,B) -> f9.2(A,B) [2 >= A] f20.7(A,B) -> f9.3(A,B) [2 >= A] f20.7(A,B) -> f9.9(A,B) [2 >= A] f12.8(A,B) -> f9.2(1 + A,B) [5 >= A] f12.8(A,B) -> f9.3(1 + A,B) [5 >= A] f12.8(A,B) -> f9.9(1 + A,B) [5 >= A] f12.8(A,B) -> f9.10(1 + A,B) [5 >= A] f9.9(A,B) -> f20.6(A,0) [5 >= A] f9.9(A,B) -> f20.7(A,0) [5 >= A] f9.10(A,B) -> f20.6(A,B) [A >= 6] f0.11(A,B) -> f9.2(C,B) True f0.11(A,B) -> f9.3(C,B) True f0.11(A,B) -> f9.9(C,B) True f0.11(A,B) -> f9.10(C,B) True Signature: {(f0.11,2);(f12.4,2);(f12.8,2);(f20.6,2);(f20.7,2);(f9.10,2);(f9.2,2);(f9.3,2);(f9.9,2)} Rule Graph: [0->{8,9,10,11},1->{8,9,10,11},2->{14},3->{3,4},4->{5,6,7},5->{0},6->{1},7->{12,13},8->{0},9->{1},10->{12 ,13},11->{14},12->{3,4},13->{5,6,7},14->{3,4},15->{0},16->{1},17->{12,13},18->{14}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f9.2(A,B) -> f12.8(A,C) [5 >= A && 0 >= 1 + C] f9.3(A,B) -> f12.8(A,C) [5 >= A && C >= 1] f12.4(A,B) -> f9.10(1 + A,B) [A >= 6] f20.6(A,B) -> f20.6(-1 + A,B) [A >= 3] f20.6(A,B) -> f20.7(-1 + A,B) [A >= 3] f20.7(A,B) -> f9.2(A,B) [2 >= A] f20.7(A,B) -> f9.3(A,B) [2 >= A] f20.7(A,B) -> f9.9(A,B) [2 >= A] f12.8(A,B) -> f9.2(1 + A,B) [5 >= A] f12.8(A,B) -> f9.3(1 + A,B) [5 >= A] f12.8(A,B) -> f9.9(1 + A,B) [5 >= A] f12.8(A,B) -> f9.10(1 + A,B) [5 >= A] f9.9(A,B) -> f20.6(A,0) [5 >= A] f9.9(A,B) -> f20.7(A,0) [5 >= A] f9.10(A,B) -> f20.6(A,B) [A >= 6] f0.11(A,B) -> f9.2(C,B) True f0.11(A,B) -> f9.3(C,B) True f0.11(A,B) -> f9.9(C,B) True f0.11(A,B) -> f9.10(C,B) True f12.8(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f20.7(A,B) -> exitus616(A,B) True f9.9(A,B) -> exitus616(A,B) True f12.8(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f20.6(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.2(A,B) -> exitus616(A,B) True Signature: {(exitus616,2);(f0.11,2);(f12.4,2);(f12.8,2);(f20.6,2);(f20.7,2);(f9.10,2);(f9.2,2);(f9.3,2);(f9.9,2)} Rule Graph: [0->{8,9,10,11,19,33,47,61,75},1->{8,9,10,11,27,41,55,69,83},2->{14},3->{3,4,22,36,50,64,78},4->{5,6,7,21 ,35,49,63,77},5->{0,20,34,48,62,76},6->{1,28,42,56,70,84},7->{12,13,24,38,52,66,80},8->{0,32,46,60,74,88} ,9->{1,29,43,57,71,85},10->{12,13,26,40,54,68,82},11->{14,31,45,59,73,87},12->{3,4,23,37,51,65,79},13->{5,6 ,7,25,39,53,67,81},14->{3,4,30,44,58,72,86},15->{0},16->{1},17->{12,13},18->{14}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88] | `- p:[0,5,4,3,12,7,13,10,1,6,9,14,11,8] c: [] MAYBE