MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f4(C,0) True (1,1) 1. f4(A,B) -> f4(A,1 + B) [B >= 0 && 0 >= 1 + C] (?,1) 2. f4(A,B) -> f4(A,1 + B) [B >= 0] (?,1) 3. f4(A,B) -> f14(A,B) [B >= 0 && A >= 0 && B >= 1 + A] (?,1) 4. f4(A,B) -> f14(A,B) [B >= 0 && 0 >= 1 + A] (?,1) 5. f4(A,B) -> f14(A,B) [B >= 0 && A >= 0 && A >= B] (?,1) 6. f4(A,B) -> f14(A,B) [B >= 0 && 0 >= 1 + C && A >= 0 && B >= 1 + A] (?,1) Signature: {(f0,2);(f14,2);(f4,2)} Flow Graph: [0->{1,2,3,4,5,6},1->{1,2,3,4,5,6},2->{1,2,3,4,5,6},3->{},4->{},5->{},6->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,3),(0,6)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f4(C,0) True (1,1) 1. f4(A,B) -> f4(A,1 + B) [B >= 0 && 0 >= 1 + C] (?,1) 2. f4(A,B) -> f4(A,1 + B) [B >= 0] (?,1) 3. f4(A,B) -> f14(A,B) [B >= 0 && A >= 0 && B >= 1 + A] (?,1) 4. f4(A,B) -> f14(A,B) [B >= 0 && 0 >= 1 + A] (?,1) 5. f4(A,B) -> f14(A,B) [B >= 0 && A >= 0 && A >= B] (?,1) 6. f4(A,B) -> f14(A,B) [B >= 0 && 0 >= 1 + C && A >= 0 && B >= 1 + A] (?,1) Signature: {(f0,2);(f14,2);(f4,2)} Flow Graph: [0->{1,2,4,5},1->{1,2,3,4,5,6},2->{1,2,3,4,5,6},3->{},4->{},5->{},6->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f0(A,B) -> f4(C,0) True f4(A,B) -> f4(A,1 + B) [B >= 0 && 0 >= 1 + C] f4(A,B) -> f4(A,1 + B) [B >= 0] f4(A,B) -> f14(A,B) [B >= 0 && A >= 0 && B >= 1 + A] f4(A,B) -> f14(A,B) [B >= 0 && 0 >= 1 + A] f4(A,B) -> f14(A,B) [B >= 0 && A >= 0 && A >= B] f4(A,B) -> f14(A,B) [B >= 0 && 0 >= 1 + C && A >= 0 && B >= 1 + A] Signature: {(f0,2);(f14,2);(f4,2)} Rule Graph: [0->{1,2,4,5},1->{1,2,3,4,5,6},2->{1,2,3,4,5,6},3->{},4->{},5->{},6->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f0.0(A,B) -> f4.1(C,0) True f0.0(A,B) -> f4.2(C,0) True f0.0(A,B) -> f4.4(C,0) True f0.0(A,B) -> f4.5(C,0) True f4.1(A,B) -> f4.1(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.2(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.3(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.4(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.5(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.6(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.2(A,B) -> f4.1(A,1 + B) [B >= 0] f4.2(A,B) -> f4.2(A,1 + B) [B >= 0] f4.2(A,B) -> f4.3(A,1 + B) [B >= 0] f4.2(A,B) -> f4.4(A,1 + B) [B >= 0] f4.2(A,B) -> f4.5(A,1 + B) [B >= 0] f4.2(A,B) -> f4.6(A,1 + B) [B >= 0] f4.3(A,B) -> f14.7(A,B) [B >= 0 && A >= 0 && B >= 1 + A] f4.4(A,B) -> f14.7(A,B) [B >= 0 && 0 >= 1 + A] f4.5(A,B) -> f14.7(A,B) [B >= 0 && A >= 0 && A >= B] f4.6(A,B) -> f14.7(A,B) [B >= 0 && 0 >= 1 + C && A >= 0 && B >= 1 + A] Signature: {(f0.0,2);(f14.7,2);(f4.1,2);(f4.2,2);(f4.3,2);(f4.4,2);(f4.5,2);(f4.6,2)} Rule Graph: [0->{4,5,6,7,8,9},1->{10,11,12,13,14,15},2->{17},3->{18},4->{4,5,6,7,8,9},5->{10,11,12,13,14,15},6->{16} ,7->{17},8->{18},9->{19},10->{4,5,6,7,8,9},11->{10,11,12,13,14,15},12->{16},13->{17},14->{18},15->{19} ,16->{},17->{},18->{},19->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f0.0(A,B) -> f4.1(C,0) True f0.0(A,B) -> f4.2(C,0) True f0.0(A,B) -> f4.4(C,0) True f0.0(A,B) -> f4.5(C,0) True f4.1(A,B) -> f4.1(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.2(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.3(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.4(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.5(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.1(A,B) -> f4.6(A,1 + B) [B >= 0 && 0 >= 1 + C] f4.2(A,B) -> f4.1(A,1 + B) [B >= 0] f4.2(A,B) -> f4.2(A,1 + B) [B >= 0] f4.2(A,B) -> f4.3(A,1 + B) [B >= 0] f4.2(A,B) -> f4.4(A,1 + B) [B >= 0] f4.2(A,B) -> f4.5(A,1 + B) [B >= 0] f4.2(A,B) -> f4.6(A,1 + B) [B >= 0] f4.3(A,B) -> f14.7(A,B) [B >= 0 && A >= 0 && B >= 1 + A] f4.4(A,B) -> f14.7(A,B) [B >= 0 && 0 >= 1 + A] f4.5(A,B) -> f14.7(A,B) [B >= 0 && A >= 0 && A >= B] f4.6(A,B) -> f14.7(A,B) [B >= 0 && 0 >= 1 + C && A >= 0 && B >= 1 + A] f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True f14.7(A,B) -> exitus616(A,B) True Signature: {(exitus616,2);(f0.0,2);(f14.7,2);(f4.1,2);(f4.2,2);(f4.3,2);(f4.4,2);(f4.5,2);(f4.6,2)} Rule Graph: [0->{4,5,6,7,8,9},1->{10,11,12,13,14,15},2->{17},3->{18},4->{4,5,6,7,8,9},5->{10,11,12,13,14,15},6->{16} ,7->{17},8->{18},9->{19},10->{4,5,6,7,8,9},11->{10,11,12,13,14,15},12->{16},13->{17},14->{18},15->{19} ,16->{25,29,33,37},17->{21,24,28,32,36},18->{20,23,27,31,35},19->{22,26,30,34}] + 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] | `- p:[4,10,5,11] c: [] MAYBE