YES(?,POLY) * Step 1: ArgumentFilter WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11} ,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}] + Applied Processor: ArgumentFilter [3,4,5,6,7,8,9,10,11,12,16,17,18,19,21,22,23] + Details: We remove following argument positions: [3,4,5,6,7,8,9,10,11,12,16,17,18,19,21,22,23]. * Step 2: UnsatRules WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f1(A,B,C,N,O,P,U) -> f1(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,N,O,P,U) -> f4(E1,D1,F1,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,N,O,P,U) -> f4(E1,D1,F1,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,N,O,P,U) -> f4(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1) 12. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1) 13. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 15. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1) 16. f3(A,B,C,N,O,P,U) -> f4(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,N,O,P,U) -> f1(A,2,Y,N,O,P,U) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11} ,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [12,15] * Step 3: UnreachableRules WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f1(A,B,C,N,O,P,U) -> f1(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,N,O,P,U) -> f4(E1,D1,F1,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,N,O,P,U) -> f4(E1,D1,F1,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,N,O,P,U) -> f4(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,N,O,P,U) -> f4(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,N,O,P,U) -> f1(A,2,Y,N,O,P,U) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10 ,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10,11},14->{7,8,9,10,11},16->{} ,17->{0,13,14}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,3,4,5,6] * Step 4: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f1(A,B,C,N,O,P,U) -> f1(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,N,O,P,U) -> f4(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,N,O,P,U) -> f4(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,N,O,P,U) -> f1(A,2,Y,N,O,P,U) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10 ,11},14->{7,8,9,10,11},16->{},17->{0,13,14}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(13,11),(14,11)] * Step 5: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f1(A,B,C,N,O,P,U) -> f1(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,N,O,P,U) -> f4(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,N,O,P,U) -> f4(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,N,O,P,U) -> f1(A,2,Y,N,O,P,U) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10} ,14->{7,8,9,10},16->{},17->{0,13,14}] + Applied Processor: FromIts + Details: () * Step 6: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: f1(A,B,C,N,O,P,U) -> f1(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,U) -> f10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,U) -> f4(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1(A,B,C,N,O,P,U) -> f10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f3(A,B,C,N,O,P,U) -> f4(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] f3(A,B,C,N,O,P,U) -> f1(A,2,Y,N,O,P,U) [A >= 2] Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Rule Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10} ,14->{7,8,9,10},16->{},17->{0,13,14}] + Applied Processor: Unfold + Details: () * Step 7: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f1.0(A,B,C,N,O,P,U) -> f1.0(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f1.0(A,B,C,N,O,P,U) -> f1.13(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f1.0(A,B,C,N,O,P,U) -> f1.14(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f10.7(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.11(A,B,C,N,O,P,U) -> f4.18(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] f1.13(A,B,C,N,O,P,U) -> f10.7(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.8(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.9(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.14(A,B,C,N,O,P,U) -> f10.7(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.8(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.9(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f3.16(A,B,C,N,O,P,U) -> f4.18(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] f3.17(A,B,C,N,O,P,U) -> f1.0(A,2,Y,N,O,P,U) [A >= 2] f3.17(A,B,C,N,O,P,U) -> f1.13(A,2,Y,N,O,P,U) [A >= 2] f3.17(A,B,C,N,O,P,U) -> f1.14(A,2,Y,N,O,P,U) [A >= 2] Signature: {(f1.0,7) ;(f1.13,7) ;(f1.14,7) ;(f10.10,7) ;(f10.11,7) ;(f10.7,7) ;(f10.8,7) ;(f10.9,7) ;(f3.16,7) ;(f3.17,7) ;(f4.18,7)} Rule Graph: [0->{0,1,2},1->{24,25,26,27},2->{28,29,30,31},3->{3,4,5,6,7},4->{8,9,10,11,12},5->{13,14,15,16,17},6->{18 ,19,20,21,22},7->{23},8->{3,4,5,6,7},9->{8,9,10,11,12},10->{13,14,15,16,17},11->{18,19,20,21,22},12->{23} ,13->{3,4,5,6,7},14->{8,9,10,11,12},15->{13,14,15,16,17},16->{18,19,20,21,22},17->{23},18->{3,4,5,6,7} ,19->{8,9,10,11,12},20->{13,14,15,16,17},21->{18,19,20,21,22},22->{23},23->{},24->{3,4,5,6,7},25->{8,9,10,11 ,12},26->{13,14,15,16,17},27->{18,19,20,21,22},28->{3,4,5,6,7},29->{8,9,10,11,12},30->{13,14,15,16,17} ,31->{18,19,20,21,22},32->{},33->{0,1,2},34->{24,25,26,27},35->{28,29,30,31}] + Applied Processor: AddSinks + Details: () * Step 8: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f1.0(A,B,C,N,O,P,U) -> f1.0(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f1.0(A,B,C,N,O,P,U) -> f1.13(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f1.0(A,B,C,N,O,P,U) -> f1.14(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f10.7(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.11(A,B,C,N,O,P,U) -> f4.18(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] f1.13(A,B,C,N,O,P,U) -> f10.7(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.8(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.9(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.14(A,B,C,N,O,P,U) -> f10.7(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.8(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.9(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f3.16(A,B,C,N,O,P,U) -> f4.18(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] f3.17(A,B,C,N,O,P,U) -> f1.0(A,2,Y,N,O,P,U) [A >= 2] f3.17(A,B,C,N,O,P,U) -> f1.13(A,2,Y,N,O,P,U) [A >= 2] f3.17(A,B,C,N,O,P,U) -> f1.14(A,2,Y,N,O,P,U) [A >= 2] f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True Signature: {(exitus616,7) ;(f1.0,7) ;(f1.13,7) ;(f1.14,7) ;(f10.10,7) ;(f10.11,7) ;(f10.7,7) ;(f10.8,7) ;(f10.9,7) ;(f3.16,7) ;(f3.17,7) ;(f4.18,7)} Rule Graph: [0->{0,1,2},1->{24,25,26,27},2->{28,29,30,31},3->{3,4,5,6,7},4->{8,9,10,11,12},5->{13,14,15,16,17},6->{18 ,19,20,21,22},7->{23},8->{3,4,5,6,7},9->{8,9,10,11,12},10->{13,14,15,16,17},11->{18,19,20,21,22},12->{23} ,13->{3,4,5,6,7},14->{8,9,10,11,12},15->{13,14,15,16,17},16->{18,19,20,21,22},17->{23},18->{3,4,5,6,7} ,19->{8,9,10,11,12},20->{13,14,15,16,17},21->{18,19,20,21,22},22->{23},23->{36,37,38,39,40,41,42,43,44,45,46 ,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82 ,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99},24->{3,4,5,6,7},25->{8,9,10,11,12},26->{13,14,15,16,17} ,27->{18,19,20,21,22},28->{3,4,5,6,7},29->{8,9,10,11,12},30->{13,14,15,16,17},31->{18,19,20,21,22},32->{100} ,33->{0,1,2},34->{24,25,26,27},35->{28,29,30,31}] + Applied Processor: Decompose Greedy + 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,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100] | +- p:[0] c: [0] | `- p:[3,8,4,13,5,18,6,11,9,14,10,19,16,15,20,21] c: [3,4,5,6,8,9,10,11,13,14,15,16,18,19,20,21] * Step 9: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f1.0(A,B,C,N,O,P,U) -> f1.0(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f1.0(A,B,C,N,O,P,U) -> f1.13(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f1.0(A,B,C,N,O,P,U) -> f1.14(A,1 + B,D,N,O,P,U) [A >= 1 + B && B >= 0] f10.7(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.7(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.8(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.9(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.7(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.8(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.9(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.10(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.10(A,B,C,N,O,P,U) -> f10.11(A1,Z,Y,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10.11(A,B,C,N,O,P,U) -> f4.18(D1,B,C,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] f1.13(A,B,C,N,O,P,U) -> f10.7(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.8(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.9(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.13(A,B,C,N,O,P,U) -> f10.10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1.14(A,B,C,N,O,P,U) -> f10.7(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.8(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.9(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1.14(A,B,C,N,O,P,U) -> f10.10(Y,1 + U,C,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f3.16(A,B,C,N,O,P,U) -> f4.18(D1,0,0,C1,O,B1,U) [0 >= D1 && 0 >= A] f3.17(A,B,C,N,O,P,U) -> f1.0(A,2,Y,N,O,P,U) [A >= 2] f3.17(A,B,C,N,O,P,U) -> f1.13(A,2,Y,N,O,P,U) [A >= 2] f3.17(A,B,C,N,O,P,U) -> f1.14(A,2,Y,N,O,P,U) [A >= 2] f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True f4.18(A,B,C,N,O,P,U) -> exitus616(A,B,C,N,O,P,U) True Signature: {(exitus616,7) ;(f1.0,7) ;(f1.13,7) ;(f1.14,7) ;(f10.10,7) ;(f10.11,7) ;(f10.7,7) ;(f10.8,7) ;(f10.9,7) ;(f3.16,7) ;(f3.17,7) ;(f4.18,7)} Rule Graph: [0->{0,1,2},1->{24,25,26,27},2->{28,29,30,31},3->{3,4,5,6,7},4->{8,9,10,11,12},5->{13,14,15,16,17},6->{18 ,19,20,21,22},7->{23},8->{3,4,5,6,7},9->{8,9,10,11,12},10->{13,14,15,16,17},11->{18,19,20,21,22},12->{23} ,13->{3,4,5,6,7},14->{8,9,10,11,12},15->{13,14,15,16,17},16->{18,19,20,21,22},17->{23},18->{3,4,5,6,7} ,19->{8,9,10,11,12},20->{13,14,15,16,17},21->{18,19,20,21,22},22->{23},23->{36,37,38,39,40,41,42,43,44,45,46 ,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82 ,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99},24->{3,4,5,6,7},25->{8,9,10,11,12},26->{13,14,15,16,17} ,27->{18,19,20,21,22},28->{3,4,5,6,7},29->{8,9,10,11,12},30->{13,14,15,16,17},31->{18,19,20,21,22},32->{100} ,33->{0,1,2},34->{24,25,26,27},35->{28,29,30,31}] ,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,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100] | +- p:[0] c: [0] | `- p:[3,8,4,13,5,18,6,11,9,14,10,19,16,15,20,21] c: [3,4,5,6,8,9,10,11,13,14,15,16,18,19,20,21]) + Applied Processor: AbstractSize Minimize + Details: () * Step 10: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,N,O,P,U,0.0,0.1] f1.0 ~> f1.0 [A <= A, B <= A, C <= unknown, N <= N, O <= O, P <= P, U <= U] f1.0 ~> f1.13 [A <= A, B <= A, C <= unknown, N <= N, O <= O, P <= P, U <= U] f1.0 ~> f1.14 [A <= A, B <= A, C <= unknown, N <= N, O <= O, P <= P, U <= U] f10.7 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.11 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.11 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.11 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.11 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.11 ~> f4.18 [A <= unknown, B <= B, C <= C, N <= unknown, O <= O, P <= unknown, U <= U] f1.13 ~> f10.7 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.13 ~> f10.8 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.13 ~> f10.9 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.13 ~> f10.10 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.14 ~> f10.7 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.14 ~> f10.8 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.14 ~> f10.9 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f1.14 ~> f10.10 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, U <= U] f3.16 ~> f4.18 [A <= unknown, B <= 0*K, C <= 0*K, N <= unknown, O <= O, P <= unknown, U <= U] f3.17 ~> f1.0 [A <= A, B <= 2*K, C <= unknown, N <= N, O <= O, P <= P, U <= U] f3.17 ~> f1.13 [A <= A, B <= 2*K, C <= unknown, N <= N, O <= O, P <= P, U <= U] f3.17 ~> f1.14 [A <= A, B <= 2*K, C <= unknown, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] f4.18 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, U <= U] + Loop: [0.0 <= K + A + B] f1.0 ~> f1.0 [A <= A, B <= A, C <= unknown, N <= N, O <= O, P <= P, U <= U] + Loop: [0.1 <= K + U] f10.7 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.7 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.7 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.8 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.8 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.9 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.9 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] f10.10 ~> f10.10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, U <= K + U] + Applied Processor: AbstractFlow + Details: () * Step 11: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,N,O,P,U,0.0,0.1] f1.0 ~> f1.0 [A ~=> B,huge ~=> C] f1.0 ~> f1.13 [A ~=> B,huge ~=> C] f1.0 ~> f1.14 [A ~=> B,huge ~=> C] f10.7 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.11 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.11 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.11 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.11 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.11 ~> f4.18 [huge ~=> A,huge ~=> N,huge ~=> P] f1.13 ~> f10.7 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.13 ~> f10.8 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.13 ~> f10.9 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.13 ~> f10.10 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.14 ~> f10.7 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.14 ~> f10.8 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.14 ~> f10.9 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f1.14 ~> f10.10 [C ~=> N,U ~=> O,K ~=> P,huge ~=> A,U ~+> B,K ~+> B] f3.16 ~> f4.18 [K ~=> B,K ~=> C,huge ~=> A,huge ~=> N,huge ~=> P] f3.17 ~> f1.0 [K ~=> B,huge ~=> C] f3.17 ~> f1.13 [K ~=> B,huge ~=> C] f3.17 ~> f1.14 [K ~=> B,huge ~=> C] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] f4.18 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f1.0 ~> f1.0 [A ~=> B,huge ~=> C] + Loop: [U ~+> 0.1,K ~+> 0.1] f10.7 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.7 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.7 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.8 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.8 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.9 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.9 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10.10 ~> f10.10 [K ~=> P,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] + Applied Processor: Lare + Details: f3.17 ~> exitus616 [U ~=> O ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> N ,huge ~=> P ,A ~+> 0.0 ,A ~+> tick ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,U ~*> 0.1 ,U ~*> tick ,K ~*> U ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] f3.16 ~> exitus616 [K ~=> B,K ~=> C,huge ~=> A,huge ~=> N,huge ~=> P] + f1.0> [A ~=> B ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] + f10.7> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.9> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.10> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.8> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.7> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.9> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.10> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.8> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.7> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.9> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.10> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.8> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.7> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.9> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.10> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] f10.8> [K ~=> P ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> 0.1 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> 0.1 ,K ~+> tick ,U ~*> U ,K ~*> U] YES(?,POLY)