MAYBE * Step 1: UnreachableRules MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D) -> f10001(A,B,C,D) True (1,1) 1. f2(A,B,C,D) -> f2(A,B,C,D) True (?,1) 2. f2(A,B,C,D) -> f10001(A,B,C,D) True (?,1) 3. f2(A,B,C,D) -> f1200(B,B,C,D) True (?,1) 4. f2200(A,B,C,D) -> f10000(A,B,0,D) [C = 0] (?,1) 5. f12(A,B,C,D) -> f12(A,B,C,D) True (?,1) 6. f100(A,B,C,D) -> f110(A,1,C,D) True (?,1) 7. f110(A,B,C,D) -> f120(A,2,C,D) True (?,1) 8. f120(A,B,C,D) -> f120(A,B,C,D) True (?,1) 9. f1200(A,B,C,D) -> f1200(A,B,C,D) True (?,1) 10. f0(A,B,C,D) -> f2(A,2,C,D) True (1,1) 11. f0(A,B,C,D) -> f10001(A,1,C,D) True (1,1) 12. f0(A,B,C,D) -> f110(1,1,C,D) True (1,1) 13. f0(A,B,C,D) -> f12(B,2,C,D) True (1,1) 14. f12(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 15. f0(A,B,C,D) -> f10001(B,B,C,1) True (1,1) 16. f0(A,B,C,D) -> f10001(B,1,C,1) True (1,1) 17. f100(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 18. f110(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 19. f120(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 20. f1000(A,B,C,D) -> f1200(A,2,C,D) True (?,1) 21. f1000(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 22. f1200(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 23. f1000(A,B,C,D) -> f10001(A,1,C,1) True (?,1) Signature: {(f0,4);(f100,4);(f1000,4);(f10000,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4);(f2200,4)} Flow Graph: [0->{},1->{1,2,3},2->{},3->{9,22},4->{},5->{5,14},6->{7,18},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3} ,11->{},12->{7,18},13->{5,14},14->{},15->{},16->{},17->{},18->{},19->{},20->{9,22},21->{},22->{},23->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [4,6,17,20,21,23] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D) -> f10001(A,B,C,D) True (1,1) 1. f2(A,B,C,D) -> f2(A,B,C,D) True (?,1) 2. f2(A,B,C,D) -> f10001(A,B,C,D) True (?,1) 3. f2(A,B,C,D) -> f1200(B,B,C,D) True (?,1) 5. f12(A,B,C,D) -> f12(A,B,C,D) True (?,1) 7. f110(A,B,C,D) -> f120(A,2,C,D) True (?,1) 8. f120(A,B,C,D) -> f120(A,B,C,D) True (?,1) 9. f1200(A,B,C,D) -> f1200(A,B,C,D) True (?,1) 10. f0(A,B,C,D) -> f2(A,2,C,D) True (1,1) 11. f0(A,B,C,D) -> f10001(A,1,C,D) True (1,1) 12. f0(A,B,C,D) -> f110(1,1,C,D) True (1,1) 13. f0(A,B,C,D) -> f12(B,2,C,D) True (1,1) 14. f12(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 15. f0(A,B,C,D) -> f10001(B,B,C,1) True (1,1) 16. f0(A,B,C,D) -> f10001(B,1,C,1) True (1,1) 18. f110(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 19. f120(A,B,C,D) -> f10001(A,B,C,1) True (?,1) 22. f1200(A,B,C,D) -> f10001(A,B,C,1) True (?,1) Signature: {(f0,4);(f100,4);(f1000,4);(f10000,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4);(f2200,4)} Flow Graph: [0->{},1->{1,2,3},2->{},3->{9,22},5->{5,14},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3},11->{},12->{7,18} ,13->{5,14},14->{},15->{},16->{},18->{},19->{},22->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks MAYBE + Considered Problem: Rules: f0(A,B,C,D) -> f10001(A,B,C,D) True f2(A,B,C,D) -> f2(A,B,C,D) True f2(A,B,C,D) -> f10001(A,B,C,D) True f2(A,B,C,D) -> f1200(B,B,C,D) True f12(A,B,C,D) -> f12(A,B,C,D) True f110(A,B,C,D) -> f120(A,2,C,D) True f120(A,B,C,D) -> f120(A,B,C,D) True f1200(A,B,C,D) -> f1200(A,B,C,D) True f0(A,B,C,D) -> f2(A,2,C,D) True f0(A,B,C,D) -> f10001(A,1,C,D) True f0(A,B,C,D) -> f110(1,1,C,D) True f0(A,B,C,D) -> f12(B,2,C,D) True f12(A,B,C,D) -> f10001(A,B,C,1) True f0(A,B,C,D) -> f10001(B,B,C,1) True f0(A,B,C,D) -> f10001(B,1,C,1) True f110(A,B,C,D) -> f10001(A,B,C,1) True f120(A,B,C,D) -> f10001(A,B,C,1) True f1200(A,B,C,D) -> f10001(A,B,C,1) True Signature: {(f0,4);(f100,4);(f1000,4);(f10000,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4);(f2200,4)} Rule Graph: [0->{},1->{1,2,3},2->{},3->{9,22},5->{5,14},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3},11->{},12->{7,18} ,13->{5,14},14->{},15->{},16->{},18->{},19->{},22->{}] + Applied Processor: AddSinks + Details: () * Step 4: Failure MAYBE + Considered Problem: Rules: f0(A,B,C,D) -> f10001(A,B,C,D) True f2(A,B,C,D) -> f2(A,B,C,D) True f2(A,B,C,D) -> f10001(A,B,C,D) True f2(A,B,C,D) -> f1200(B,B,C,D) True f12(A,B,C,D) -> f12(A,B,C,D) True f110(A,B,C,D) -> f120(A,2,C,D) True f120(A,B,C,D) -> f120(A,B,C,D) True f1200(A,B,C,D) -> f1200(A,B,C,D) True f0(A,B,C,D) -> f2(A,2,C,D) True f0(A,B,C,D) -> f10001(A,1,C,D) True f0(A,B,C,D) -> f110(1,1,C,D) True f0(A,B,C,D) -> f12(B,2,C,D) True f12(A,B,C,D) -> f10001(A,B,C,1) True f0(A,B,C,D) -> f10001(B,B,C,1) True f0(A,B,C,D) -> f10001(B,1,C,1) True f110(A,B,C,D) -> f10001(A,B,C,1) True f120(A,B,C,D) -> f10001(A,B,C,1) True f1200(A,B,C,D) -> f10001(A,B,C,1) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True f10001(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(exitus616,4) ;(f0,4) ;(f100,4) ;(f1000,4) ;(f10000,4) ;(f10001,4) ;(f110,4) ;(f12,4) ;(f120,4) ;(f1200,4) ;(f2,4) ;(f2200,4)} Rule Graph: [0->{31},1->{1,2,3},2->{30},3->{9,22},5->{5,14},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3},11->{28},12->{7 ,18},13->{5,14},14->{25},15->{24},16->{23},18->{26},19->{27},22->{29}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,5,7,8,9,10,11,12,13,14,15,16,18,19,22,23,24,25,26,27,28,29,30,31] | +- p:[8] c: [] | +- p:[5] c: [] | +- p:[1] c: [] | `- p:[9] c: [] MAYBE