MAYBE * Step 1: UnreachableRules MAYBE + Considered Problem: Rules: 0. f9(A,B) -> f10(A,B) [5 >= A] (?,1) 1. f25(A,B) -> f2(A,B) True (?,1) 2. f2(A,B) -> f2(A,B) True (?,1) 3. f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] (?,1) 4. f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] (?,1) 5. f10(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 6. f27(A,B) -> f29(A,B) True (?,1) 7. f19(A,B) -> f19(-1 + A,B) [A >= 3] (?,1) 8. f19(A,B) -> f9(A,B) [2 >= A] (?,1) 9. f10(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 10. f9(A,B) -> f19(A,0) [A >= 6] (?,1) 11. f0(A,B) -> f9(C,B) True (1,1) Signature: {(f0,2);(f10,2);(f19,2);(f2,2);(f25,2);(f27,2);(f29,2);(f9,2)} Flow Graph: [0->{5,9},1->{2},2->{2},3->{5,9},4->{5,9},5->{0,3,4,10},6->{},7->{7,8},8->{0,3,4,10},9->{0,3,4,10},10->{7 ,8},11->{0,3,4,10}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,6] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B) -> f10(A,B) [5 >= A] (?,1) 3. f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] (?,1) 4. f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] (?,1) 5. f10(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 7. f19(A,B) -> f19(-1 + A,B) [A >= 3] (?,1) 8. f19(A,B) -> f9(A,B) [2 >= A] (?,1) 9. f10(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 10. f9(A,B) -> f19(A,0) [A >= 6] (?,1) 11. f0(A,B) -> f9(C,B) True (1,1) Signature: {(f0,2);(f10,2);(f19,2);(f2,2);(f25,2);(f27,2);(f29,2);(f9,2)} Flow Graph: [0->{5,9},3->{5,9},4->{5,9},5->{0,3,4,10},7->{7,8},8->{0,3,4,10},9->{0,3,4,10},10->{7,8},11->{0,3,4,10}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,5),(3,9),(4,9),(5,0),(8,3),(8,4),(8,10),(10,8)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f9(A,B) -> f10(A,B) [5 >= A] (?,1) 3. f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] (?,1) 4. f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] (?,1) 5. f10(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 7. f19(A,B) -> f19(-1 + A,B) [A >= 3] (?,1) 8. f19(A,B) -> f9(A,B) [2 >= A] (?,1) 9. f10(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 10. f9(A,B) -> f19(A,0) [A >= 6] (?,1) 11. f0(A,B) -> f9(C,B) True (1,1) Signature: {(f0,2);(f10,2);(f19,2);(f2,2);(f25,2);(f27,2);(f29,2);(f9,2)} Flow Graph: [0->{9},3->{5},4->{5},5->{3,4,10},7->{7,8},8->{0},9->{0,3,4,10},10->{7},11->{0,3,4,10}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f9(A,B) -> f10(A,B) [5 >= A] f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] f10(A,B) -> f9(1 + A,B) [A >= 6] f19(A,B) -> f19(-1 + A,B) [A >= 3] f19(A,B) -> f9(A,B) [2 >= A] f10(A,B) -> f9(1 + A,B) [5 >= A] f9(A,B) -> f19(A,0) [A >= 6] f0(A,B) -> f9(C,B) True Signature: {(f0,2);(f10,2);(f19,2);(f2,2);(f25,2);(f27,2);(f29,2);(f9,2)} Rule Graph: [0->{9},3->{5},4->{5},5->{3,4,10},7->{7,8},8->{0},9->{0,3,4,10},10->{7},11->{0,3,4,10}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f9.0(A,B) -> f10.9(A,B) [5 >= A] f9.3(A,B) -> f10.5(A,C) [A >= 6 && 0 >= 1 + C] f9.4(A,B) -> f10.5(A,C) [A >= 6 && C >= 1] f10.5(A,B) -> f9.3(1 + A,B) [A >= 6] f10.5(A,B) -> f9.4(1 + A,B) [A >= 6] f10.5(A,B) -> f9.10(1 + A,B) [A >= 6] f19.7(A,B) -> f19.7(-1 + A,B) [A >= 3] f19.7(A,B) -> f19.8(-1 + A,B) [A >= 3] f19.8(A,B) -> f9.0(A,B) [2 >= A] f10.9(A,B) -> f9.0(1 + A,B) [5 >= A] f10.9(A,B) -> f9.3(1 + A,B) [5 >= A] f10.9(A,B) -> f9.4(1 + A,B) [5 >= A] f10.9(A,B) -> f9.10(1 + A,B) [5 >= A] f9.10(A,B) -> f19.7(A,0) [A >= 6] f0.11(A,B) -> f9.0(C,B) True f0.11(A,B) -> f9.3(C,B) True f0.11(A,B) -> f9.4(C,B) True f0.11(A,B) -> f9.10(C,B) True Signature: {(f0.11,2);(f10.5,2);(f10.9,2);(f19.7,2);(f19.8,2);(f9.0,2);(f9.10,2);(f9.3,2);(f9.4,2)} Rule Graph: [0->{9,10,11,12},1->{3,4,5},2->{3,4,5},3->{1},4->{2},5->{13},6->{6,7},7->{8},8->{0},9->{0},10->{1},11->{2} ,12->{13},13->{6,7},14->{0},15->{1},16->{2},17->{13}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f9.0(A,B) -> f10.9(A,B) [5 >= A] f9.3(A,B) -> f10.5(A,C) [A >= 6 && 0 >= 1 + C] f9.4(A,B) -> f10.5(A,C) [A >= 6 && C >= 1] f10.5(A,B) -> f9.3(1 + A,B) [A >= 6] f10.5(A,B) -> f9.4(1 + A,B) [A >= 6] f10.5(A,B) -> f9.10(1 + A,B) [A >= 6] f19.7(A,B) -> f19.7(-1 + A,B) [A >= 3] f19.7(A,B) -> f19.8(-1 + A,B) [A >= 3] f19.8(A,B) -> f9.0(A,B) [2 >= A] f10.9(A,B) -> f9.0(1 + A,B) [5 >= A] f10.9(A,B) -> f9.3(1 + A,B) [5 >= A] f10.9(A,B) -> f9.4(1 + A,B) [5 >= A] f10.9(A,B) -> f9.10(1 + A,B) [5 >= A] f9.10(A,B) -> f19.7(A,0) [A >= 6] f0.11(A,B) -> f9.0(C,B) True f0.11(A,B) -> f9.3(C,B) True f0.11(A,B) -> f9.4(C,B) True f0.11(A,B) -> f9.10(C,B) True f10.9(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f19.8(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f10.9(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f19.8(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f10.9(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f19.8(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f10.9(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True f19.8(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f19.7(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f10.5(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.4(A,B) -> exitus616(A,B) True f9.3(A,B) -> exitus616(A,B) True f9.10(A,B) -> exitus616(A,B) True f9.0(A,B) -> exitus616(A,B) True Signature: {(exitus616,2);(f0.11,2);(f10.5,2);(f10.9,2);(f19.7,2);(f19.8,2);(f9.0,2);(f9.10,2);(f9.3,2);(f9.4,2)} Rule Graph: [0->{9,10,11,12,18,32,46,60},1->{3,4,5,24,38,52,66},2->{3,4,5,26,40,54,68},3->{1,25,39,53,67},4->{2,27,41 ,55,69},5->{13,23,37,51,65},6->{6,7,21,35,49,63},7->{8,20,34,48,62},8->{0,19,33,47,61},9->{0,31,45,59,73} ,10->{1,29,43,57,71},11->{2,28,42,56,70},12->{13,30,44,58,72},13->{6,7,22,36,50,64},14->{0},15->{1},16->{2} ,17->{13}] + 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] | `- p:[0,8,7,6,13,5,1,3,2,4,11,10,12,9] c: [] MAYBE