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