MAYBE * Step 1: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: 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,1) 3. f2(A,B,C,D) -> f1200(B,B,C,D) True (1,1) 4. f2200(A,B,C,D) -> f10000(A,B,0,D) [C = 0] (1,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,1) 7. f110(A,B,C,D) -> f120(A,2,C,D) True (1,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,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,1) 18. f110(A,B,C,D) -> f10001(A,B,C,1) True (1,1) 19. f120(A,B,C,D) -> f10001(A,B,C,1) True (1,1) 20. f1000(A,B,C,D) -> f1200(A,2,C,D) True (1,1) 21. f1000(A,B,C,D) -> f10001(A,B,C,1) True (1,1) 22. f1200(A,B,C,D) -> f10001(A,B,C,1) True (1,1) 23. f1000(A,B,C,D) -> f10001(A,1,C,1) True (1,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 3: AddSinks 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,1) 3. f2(A,B,C,D) -> f1200(B,B,C,D) True (1,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,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,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,1) 19. f120(A,B,C,D) -> f10001(A,B,C,1) True (1,1) 22. f1200(A,B,C,D) -> f10001(A,B,C,1) True (1,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: AddSinks + Details: () * Step 4: Failure 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) 23. f0(A,B,C,D) -> exitus616(A,B,C,D) True (1,1) 24. f12(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 25. f110(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 26. f120(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 27. f1200(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 28. f2(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 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)} Flow Graph: [0->{},1->{1,2,3,28},2->{},3->{9,22,27},5->{5,14,24},7->{8,19,26},8->{8,19,26},9->{9,22,27},10->{1,2,3,28} ,11->{},12->{7,18,25},13->{5,14,24},14->{},15->{},16->{},18->{},19->{},22->{},23->{},24->{},25->{},26->{} ,27->{},28->{}] + Applied Processor: LooptreeTransformer + 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] | +- p:[8] c: [] | +- p:[5] c: [] | +- p:[1] c: [] | `- p:[9] c: [] MAYBE