MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D) -> f10001(B,1,C,1) True (1,1) 1. f0(A,B,C,D) -> f10001(B,B,C,1) True (1,1) 2. f0(A,B,C,D) -> f12(B,2,C,D) True (1,1) 3. f0(A,B,C,D) -> f110(1,1,C,D) True (1,1) 4. f0(A,B,C,D) -> f10001(A,1,C,D) True (1,1) 5. f0(A,B,C,D) -> f2(A,2,C,D) True (1,1) 6. f0(A,B,C,D) -> f10001(A,B,C,D) True (1,1) 7. f12(A,B,C,D) -> f10001(A,B,C,1) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 8. f12(A,B,C,D) -> f12(A,B,C,D) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 9. f110(A,B,C,D) -> f10001(A,B,C,1) [1 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 10. f110(A,B,C,D) -> f120(A,2,C,D) [1 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 11. f2(A,B,C,D) -> f1200(B,B,C,D) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 12. f2(A,B,C,D) -> f10001(A,B,C,D) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 13. f2(A,B,C,D) -> f2(A,B,C,D) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 14. f120(A,B,C,D) -> f10001(A,B,C,1) [2 + -1*B >= 0 (?,1) && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 15. f120(A,B,C,D) -> f120(A,B,C,D) [2 + -1*B >= 0 (?,1) && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 16. f1200(A,B,C,D) -> f10001(A,B,C,1) [2 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] 17. f1200(A,B,C,D) -> f1200(A,B,C,D) [2 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] Signature: {(f0,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4)} Flow Graph: [0->{},1->{},2->{7,8},3->{9,10},4->{},5->{11,12,13},6->{},7->{},8->{7,8},9->{},10->{14,15},11->{16,17} ,12->{},13->{11,12,13},14->{},15->{14,15},16->{},17->{16,17}] + Applied Processor: ArgumentFilter [2,3] + Details: We remove following argument positions: [2,3]. * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f10001(B,1) True (1,1) 1. f0(A,B) -> f10001(B,B) True (1,1) 2. f0(A,B) -> f12(B,2) True (1,1) 3. f0(A,B) -> f110(1,1) True (1,1) 4. f0(A,B) -> f10001(A,1) True (1,1) 5. f0(A,B) -> f2(A,2) True (1,1) 6. f0(A,B) -> f10001(A,B) True (1,1) 7. f12(A,B) -> f10001(A,B) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 8. f12(A,B) -> f12(A,B) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 9. f110(A,B) -> f10001(A,B) [1 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 10. f110(A,B) -> f120(A,2) [1 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 11. f2(A,B) -> f1200(B,B) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 12. f2(A,B) -> f10001(A,B) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 13. f2(A,B) -> f2(A,B) [2 + -1*B >= 0 && -2 + B >= 0] (?,1) 14. f120(A,B) -> f10001(A,B) [2 + -1*B >= 0 (?,1) && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 15. f120(A,B) -> f120(A,B) [2 + -1*B >= 0 (?,1) && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 16. f1200(A,B) -> f10001(A,B) [2 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] 17. f1200(A,B) -> f1200(A,B) [2 + -1*B >= 0 (?,1) && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] Signature: {(f0,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4)} Flow Graph: [0->{},1->{},2->{7,8},3->{9,10},4->{},5->{11,12,13},6->{},7->{},8->{7,8},9->{},10->{14,15},11->{16,17} ,12->{},13->{11,12,13},14->{},15->{14,15},16->{},17->{16,17}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks MAYBE + Considered Problem: Rules: f0(A,B) -> f10001(B,1) True f0(A,B) -> f10001(B,B) True f0(A,B) -> f12(B,2) True f0(A,B) -> f110(1,1) True f0(A,B) -> f10001(A,1) True f0(A,B) -> f2(A,2) True f0(A,B) -> f10001(A,B) True f12(A,B) -> f10001(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f12(A,B) -> f12(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f110(A,B) -> f10001(A,B) [1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f110(A,B) -> f120(A,2) [1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f2(A,B) -> f1200(B,B) [2 + -1*B >= 0 && -2 + B >= 0] f2(A,B) -> f10001(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f2(A,B) -> f2(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f120(A,B) -> f10001(A,B) [2 + -1*B >= 0 && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f120(A,B) -> f120(A,B) [2 + -1*B >= 0 && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f1200(A,B) -> f10001(A,B) [2 + -1*B >= 0 && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] f1200(A,B) -> f1200(A,B) [2 + -1*B >= 0 && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] Signature: {(f0,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4)} Rule Graph: [0->{},1->{},2->{7,8},3->{9,10},4->{},5->{11,12,13},6->{},7->{},8->{7,8},9->{},10->{14,15},11->{16,17} ,12->{},13->{11,12,13},14->{},15->{14,15},16->{},17->{16,17}] + Applied Processor: AddSinks + Details: () * Step 4: Failure MAYBE + Considered Problem: Rules: f0(A,B) -> f10001(B,1) True f0(A,B) -> f10001(B,B) True f0(A,B) -> f12(B,2) True f0(A,B) -> f110(1,1) True f0(A,B) -> f10001(A,1) True f0(A,B) -> f2(A,2) True f0(A,B) -> f10001(A,B) True f12(A,B) -> f10001(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f12(A,B) -> f12(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f110(A,B) -> f10001(A,B) [1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f110(A,B) -> f120(A,2) [1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f2(A,B) -> f1200(B,B) [2 + -1*B >= 0 && -2 + B >= 0] f2(A,B) -> f10001(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f2(A,B) -> f2(A,B) [2 + -1*B >= 0 && -2 + B >= 0] f120(A,B) -> f10001(A,B) [2 + -1*B >= 0 && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f120(A,B) -> f120(A,B) [2 + -1*B >= 0 && 1 + A + -1*B >= 0 && 3 + -1*A + -1*B >= 0 && -2 + B >= 0 && -3 + A + B >= 0 && -1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] f1200(A,B) -> f10001(A,B) [2 + -1*B >= 0 && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] f1200(A,B) -> f1200(A,B) [2 + -1*B >= 0 && A + -1*B >= 0 && 4 + -1*A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0] f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True f10001(A,B) -> exitus616(A,B) True Signature: {(exitus616,2);(f0,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4)} Rule Graph: [0->{26},1->{25},2->{7,8},3->{9,10},4->{21},5->{11,12,13},6->{18},7->{24},8->{7,8},9->{23},10->{14,15} ,11->{16,17},12->{19},13->{11,12,13},14->{22},15->{14,15},16->{20},17->{16,17}] + 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] | +- p:[13] c: [] | +- p:[17] c: [] | +- p:[15] c: [] | `- p:[8] c: [] MAYBE