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