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