MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [0 >= A] (?,1) 1. f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) True (?,1) 2. f13(A,B,C,D,E,F) -> f400(A,B,C,D,E,F) [B >= 1 + A] (?,1) 3. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] (1,1) 4. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] (1,1) 5. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [E >= C] (?,1) 6. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [C >= 1 + E] (?,1) 7. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,F) [H >= C && 0 >= B && A >= 1] (?,1) 8. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,0) [H >= C && B >= 1 && A >= 1] (?,1) 9. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [E >= C] (?,1) 10. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C >= 1 + E] (?,1) 11. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,F) [H >= C && 0 >= C && 0 >= B] (?,1) 12. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,0) [H >= C && 0 >= C && B >= 1] (?,1) 13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F) [C = E] (?,1) 14. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C >= 1 + E] (?,1) 15. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,F) [1 + H >= C && C >= 1 && 0 >= B] (?,1) 16. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,0) [1 + H >= C && C >= 1 && B >= 1] (?,1) 17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F) [E >= C] (?,1) 18. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1) [C >= 1 + E] (?,1) 19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [0 >= B && H >= E] (?,1) 20. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [B >= 1 && H >= E] (?,1) 21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [E >= C] (?,1) 22. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C >= 1 + E] (?,1) 23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [0 >= B && H >= E] (?,1) 24. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [B >= 1 && H >= E] (?,1) 25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [E >= C] (?,1) 26. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C >= 1 + E] (?,1) Signature: {(f13,6) ;(f14,6) ;(f2,6) ;(f23,6) ;(f33,6) ;(f4,6) ;(f400,6) ;(f43,6) ;(f53,6) ;(f6,6) ;(f61,6) ;(f63,6) ;(f71,6) ;(f73,6)} Flow Graph: [0->{},1->{0,7,8},2->{},3->{5,6},4->{5,6},5->{0,7,8},6->{0,7,8},7->{9,10},8->{9,10},9->{11,12,15,16} ,10->{11,12,15,16},11->{13,14},12->{13,14},13->{11,12,15,16},14->{11,12,15,16},15->{17,18},16->{17,18} ,17->{19,20},18->{19,20},19->{21,22},20->{21,22},21->{23,24},22->{23,24},23->{25,26},24->{25,26},25->{1,2} ,26->{1,2}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [0 >= A] (1,1) 1. f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) True (?,1) 2. f13(A,B,C,D,E,F) -> f400(A,B,C,D,E,F) [B >= 1 + A] (1,1) 3. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] (1,1) 4. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] (1,1) 5. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [E >= C] (1,1) 6. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [C >= 1 + E] (1,1) 7. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,F) [H >= C && 0 >= B && A >= 1] (?,1) 8. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,0) [H >= C && B >= 1 && A >= 1] (?,1) 9. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [E >= C] (?,1) 10. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C >= 1 + E] (?,1) 11. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,F) [H >= C && 0 >= C && 0 >= B] (?,1) 12. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,0) [H >= C && 0 >= C && B >= 1] (?,1) 13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F) [C = E] (?,1) 14. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C >= 1 + E] (?,1) 15. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,F) [1 + H >= C && C >= 1 && 0 >= B] (?,1) 16. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,0) [1 + H >= C && C >= 1 && B >= 1] (?,1) 17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F) [E >= C] (?,1) 18. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1) [C >= 1 + E] (?,1) 19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [0 >= B && H >= E] (?,1) 20. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [B >= 1 && H >= E] (?,1) 21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [E >= C] (?,1) 22. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C >= 1 + E] (?,1) 23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [0 >= B && H >= E] (?,1) 24. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [B >= 1 && H >= E] (?,1) 25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [E >= C] (?,1) 26. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C >= 1 + E] (?,1) Signature: {(f13,6) ;(f14,6) ;(f2,6) ;(f23,6) ;(f33,6) ;(f4,6) ;(f400,6) ;(f43,6) ;(f53,6) ;(f6,6) ;(f61,6) ;(f63,6) ;(f71,6) ;(f73,6)} Flow Graph: [0->{},1->{0,7,8},2->{},3->{5,6},4->{5,6},5->{0,7,8},6->{0,7,8},7->{9,10},8->{9,10},9->{11,12,15,16} ,10->{11,12,15,16},11->{13,14},12->{13,14},13->{11,12,15,16},14->{11,12,15,16},15->{17,18},16->{17,18} ,17->{19,20},18->{19,20},19->{21,22},20->{21,22},21->{23,24},22->{23,24},23->{25,26},24->{25,26},25->{1,2} ,26->{1,2}] + Applied Processor: AddSinks + Details: () * Step 3: Failure MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [0 >= A] (?,1) 1. f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) True (?,1) 2. f13(A,B,C,D,E,F) -> f400(A,B,C,D,E,F) [B >= 1 + A] (?,1) 3. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] (1,1) 4. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] (1,1) 5. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [E >= C] (?,1) 6. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [C >= 1 + E] (?,1) 7. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,F) [H >= C && 0 >= B && A >= 1] (?,1) 8. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,0) [H >= C && B >= 1 && A >= 1] (?,1) 9. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [E >= C] (?,1) 10. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C >= 1 + E] (?,1) 11. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,F) [H >= C && 0 >= C && 0 >= B] (?,1) 12. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,0) [H >= C && 0 >= C && B >= 1] (?,1) 13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F) [C = E] (?,1) 14. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C >= 1 + E] (?,1) 15. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,F) [1 + H >= C && C >= 1 && 0 >= B] (?,1) 16. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,0) [1 + H >= C && C >= 1 && B >= 1] (?,1) 17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F) [E >= C] (?,1) 18. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1) [C >= 1 + E] (?,1) 19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [0 >= B && H >= E] (?,1) 20. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [B >= 1 && H >= E] (?,1) 21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [E >= C] (?,1) 22. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C >= 1 + E] (?,1) 23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [0 >= B && H >= E] (?,1) 24. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [B >= 1 && H >= E] (?,1) 25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [E >= C] (?,1) 26. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C >= 1 + E] (?,1) 27. f13(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 28. f4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) Signature: {(exitus616,6) ;(f13,6) ;(f14,6) ;(f2,6) ;(f23,6) ;(f33,6) ;(f4,6) ;(f400,6) ;(f43,6) ;(f53,6) ;(f6,6) ;(f61,6) ;(f63,6) ;(f71,6) ;(f73,6)} Flow Graph: [0->{},1->{0,7,8,28},2->{},3->{5,6},4->{5,6},5->{0,7,8,28},6->{0,7,8,28},7->{9,10},8->{9,10},9->{11,12,15 ,16},10->{11,12,15,16},11->{13,14},12->{13,14},13->{11,12,15,16},14->{11,12,15,16},15->{17,18},16->{17,18} ,17->{19,20},18->{19,20},19->{21,22},20->{21,22},21->{23,24},22->{23,24},23->{25,26},24->{25,26},25->{1,2 ,27},26->{1,2,27},27->{},28->{}] + 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,24,25,26,27,28] | `- p:[1,25,23,21,19,17,15,9,7,8,10,13,11,14,12,16,18,20,22,24,26] c: [8] | `- p:[1,25,23,21,19,17,15,9,7,10,13,11,14,12,16,18,20,22,24,26] c: [18] | `- p:[1,25,23,21,19,17,15,9,7,10,13,11,14,12,16,20,22,24,26] c: [10] | `- p:[1,25,23,21,19,17,15,9,7,13,11,14,12,16,20,22,24,26] c: [15] | `- p:[1,25,23,21,19,17,16,9,7,13,11,14,12,20,22,24,26] c: [26] | `- p:[1,25,23,21,19,17,16,9,7,13,11,14,12,20,22,24] c: [25] | `- p:[11,13,12,14] c: [] MAYBE