MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (?,1) Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (1,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (1,1) Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3),(2,16)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (1,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (1,1) Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{16},2->{3},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16},9->{7,8} ,10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (?,1) 17. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) 18. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) 19. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) Signature: {(exitus616,18);(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{3,16,18},2->{3,16,18},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12,17},6->{6,9},7->{7,8} ,8->{3,16,18},9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12,17},14->{5,10,11,12,17},15->{5,10,11,12 ,17},16->{},17->{},18->{},19->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3),(2,16)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (?,1) 17. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) 18. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) 19. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) Signature: {(exitus616,18);(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{16,18},2->{3,18},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12,17},6->{6,9},7->{7,8},8->{3,16 ,18},9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12,17},14->{5,10,11,12,17},15->{5,10,11,12,17},16->{} ,17->{},18->{},19->{}] + 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] | `- p:[3,8,7,9,6,11,5,13,4,14,15,12] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | `- p:[7] c: [7] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (?,1) 17. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) 18. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) 19. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) Signature: {(exitus616,18);(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{16,18},2->{3,18},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12,17},6->{6,9},7->{7,8},8->{3,16 ,18},9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12,17},14->{5,10,11,12,17},15->{5,10,11,12,17},16->{} ,17->{},18->{},19->{}] ,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] | `- p:[3,8,7,9,6,11,5,13,4,14,15,12] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | `- p:[7] c: [7]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0.0,0.0.0,0.0.1,0.0.2,0.0.3] f0 ~> f13 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f0 ~> f17 [A <= A, B <= K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f0 ~> f17 [A <= A, B <= K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f17 ~> f23 [A <= A, B <= B, C <= K + B, D <= unknown, E <= unknown, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f23 [A <= A, B <= B, C <= C, D <= unknown, E <= unknown, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f46 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f60 ~> f60 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= unknown, N <= unknown, O <= unknown, P <= K, Q <= Q, R <= R] f60 ~> f17 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f46 ~> f60 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= H, I <= I, J <= unknown, K <= B, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= unknown, R <= unknown] f33 ~> f13 [A <= A, B <= B, C <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= 0*K, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f17 ~> f13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f17 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f0 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.0 <= 2*K + A + B] f17 ~> f23 [A <= A, B <= B, C <= K + B, D <= unknown, E <= unknown, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f60 ~> f17 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f60 ~> f60 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= unknown, N <= unknown, O <= unknown, P <= K, Q <= Q, R <= R] f46 ~> f60 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= H, I <= I, J <= unknown, K <= B, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= unknown, R <= unknown] f46 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f23 [A <= A, B <= B, C <= C, D <= unknown, E <= unknown, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f23 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= 0*K, F <= K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f33 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.0.0 <= K + B + F] f23 ~> f23 [A <= A, B <= B, C <= C, D <= unknown, E <= unknown, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.0.1 <= K + B + F] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.0.2 <= K + B + F] f46 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= unknown, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.0.3 <= K + F + J] f60 ~> f60 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= unknown, N <= unknown, O <= unknown, P <= K, Q <= Q, R <= R] + Applied Processor: FlowAbstraction + Details: () * Step 8: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0.0,0.0.0,0.0.1,0.0.2,0.0.3] f0 ~> f13 [K ~=> A] f0 ~> f17 [K ~=> B] f0 ~> f17 [K ~=> B] f17 ~> f23 [K ~=> F,huge ~=> D,huge ~=> E,B ~+> C,K ~+> C] f23 ~> f23 [huge ~=> D,huge ~=> E,F ~+> F,K ~+> F] f33 ~> f33 [F ~+> F,K ~+> F] f46 ~> f46 [huge ~=> G,huge ~=> H,huge ~=> I,F ~+> F,K ~+> F] f60 ~> f60 [K ~=> P,huge ~=> L,huge ~=> M,huge ~=> N,huge ~=> O,F ~+> F,K ~+> K,K ~+> F,K ~+> K] f60 ~> f17 [B ~+> B,K ~+> B] f46 ~> f60 [B ~=> K,K ~=> F,huge ~=> J,huge ~=> Q,huge ~=> R] f33 ~> f13 [A ~=> C] f33 ~> f46 [K ~=> F,huge ~=> G,huge ~=> H,huge ~=> I] f33 ~> f46 [K ~=> F,huge ~=> G,huge ~=> H,huge ~=> I] f23 ~> f33 [K ~=> F] f23 ~> f33 [K ~=> F] f23 ~> f33 [K ~=> E,K ~=> F] f17 ~> f13 [] f33 ~> exitus616 [] f17 ~> exitus616 [] f0 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] f17 ~> f23 [K ~=> F,huge ~=> D,huge ~=> E,B ~+> C,K ~+> C] f60 ~> f17 [B ~+> B,K ~+> B] f60 ~> f60 [K ~=> P,huge ~=> L,huge ~=> M,huge ~=> N,huge ~=> O,F ~+> F,K ~+> K,K ~+> F,K ~+> K] f46 ~> f60 [B ~=> K,K ~=> F,huge ~=> J,huge ~=> Q,huge ~=> R] f46 ~> f46 [huge ~=> G,huge ~=> H,huge ~=> I,F ~+> F,K ~+> F] f33 ~> f46 [K ~=> F,huge ~=> G,huge ~=> H,huge ~=> I] f33 ~> f33 [F ~+> F,K ~+> F] f23 ~> f33 [K ~=> F] f23 ~> f23 [huge ~=> D,huge ~=> E,F ~+> F,K ~+> F] f23 ~> f33 [K ~=> F] f23 ~> f33 [K ~=> E,K ~=> F] f33 ~> f46 [K ~=> F,huge ~=> G,huge ~=> H,huge ~=> I] + Loop: [B ~+> 0.0.0,F ~+> 0.0.0,K ~+> 0.0.0] f23 ~> f23 [huge ~=> D,huge ~=> E,F ~+> F,K ~+> F] + Loop: [B ~+> 0.0.1,F ~+> 0.0.1,K ~+> 0.0.1] f33 ~> f33 [F ~+> F,K ~+> F] + Loop: [B ~+> 0.0.2,F ~+> 0.0.2,K ~+> 0.0.2] f46 ~> f46 [huge ~=> G,huge ~=> H,huge ~=> I,F ~+> F,K ~+> F] + Loop: [F ~+> 0.0.3,J ~+> 0.0.3,K ~+> 0.0.3] f60 ~> f60 [K ~=> P,huge ~=> L,huge ~=> M,huge ~=> N,huge ~=> O,F ~+> F,K ~+> K,K ~+> F,K ~+> K] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE