YES(?,POLY) * Step 1: ArgumentFilter WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f23(0,0,2*D,D,4*D,3 + 4*D,4 + 4*D,D,B1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + C] (?,1) 2. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f23(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && 0 >= C1 && C >= J] (?,1) 3. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f23(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C1 >= 2 && C >= J] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f23(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C >= J] (?,1) 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D && P = 0] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && P >= 1 && J >= 1 + D] (?,1) 7. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && 0 >= 1 + P && J >= 1 + D] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f33(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && D >= J] (?,1) 9. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f117(A,B1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && O >= 1 + N] 10. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N >= O] (?,1) 11. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D] 12. f117(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f125(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + -1*N + O >= 0 && J >= 1 + D] 13. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && Q >= 1] 14. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f66(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= Q && P = 0] 15. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && P >= 1 && 0 >= Q] 16. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= 1 + P && 0 >= Q] 17. f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f87(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && D1 >= 1 && J >= 1 + C] 18. f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f87(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + D1 && J >= 1 + C] 19. f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f87(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + C] 20. f66(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && J >= 1 + E] 21. f66(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f66(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && E >= J] 22. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 23. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,C + Q) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 24. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L >= 1] 25. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + L] 26. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L = 0] 27. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*A1 + C >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 28. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + D] Signature: {(f0,27) ;(f117,27) ;(f125,27) ;(f23,27) ;(f33,27) ;(f39,27) ;(f44,27) ;(f46,27) ;(f49,27) ;(f54,27) ;(f60,27) ;(f66,27) ;(f72,27) ;(f87,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14,15,16},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10}] + Applied Processor: ArgumentFilter [0,5,6,8,10,12,17,18,19,20,21,22,23,24,25] + Details: We remove following argument positions: [0,5,6,8,10,12,17,18,19,20,21,22,23,24,25]. * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(0,2*D,D,4*D,D,J,L,N,O,P,Q,A1) True (1,1) 1. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + C] (?,1) 2. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && 0 >= C1 && C >= J] (?,1) 3. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C1 >= 2 && C >= J] (?,1) 4. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C >= J] (?,1) 5. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D && P = 0] (?,1) 6. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && P >= 1 && J >= 1 + D] (?,1) 7. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && 0 >= 1 + P && J >= 1 + D] (?,1) 8. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,1 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && D >= J] (?,1) 9. f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f117(B1,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && O >= 1 + N] 10. f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N >= O] (?,1) 11. f39(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D] 12. f117(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f125(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + -1*N + O >= 0 && J >= 1 + D] 13. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f72(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && Q >= 1] 14. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= Q && P = 0] 15. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && P >= 1 && 0 >= Q] 16. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= 1 + P && 0 >= Q] 17. f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && D1 >= 1 && J >= 1 + C] 18. f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + D1 && J >= 1 + C] 19. f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + C] 20. f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && J >= 1 + E] 21. f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,2 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && E >= J] 22. f49(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f54(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 23. f54(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f60(B,C,D,E,H,J,L,N,O,P,Q,C + Q) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 24. f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L >= 1] 25. f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + L] 26. f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,0,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L = 0] 27. f60(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*A1 + C >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 28. f91(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(A + B,C,D,E,H,J,L,N,1 + O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + D] Signature: {(f0,27) ;(f117,27) ;(f125,27) ;(f23,27) ;(f33,27) ;(f39,27) ;(f44,27) ;(f46,27) ;(f49,27) ;(f54,27) ;(f60,27) ;(f66,27) ;(f72,27) ;(f87,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14,15,16},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(20,15),(20,16)] * Step 3: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(0,2*D,D,4*D,D,J,L,N,O,P,Q,A1) True (1,1) 1. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + C] (?,1) 2. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && 0 >= C1 && C >= J] (?,1) 3. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C1 >= 2 && C >= J] (?,1) 4. f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C >= J] (?,1) 5. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D && P = 0] (?,1) 6. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && P >= 1 && J >= 1 + D] (?,1) 7. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && 0 >= 1 + P && J >= 1 + D] (?,1) 8. f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,1 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && D >= J] (?,1) 9. f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f117(B1,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && O >= 1 + N] 10. f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N >= O] (?,1) 11. f39(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D] 12. f117(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f125(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + -1*N + O >= 0 && J >= 1 + D] 13. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f72(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && Q >= 1] 14. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= Q && P = 0] 15. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && P >= 1 && 0 >= Q] 16. f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= 1 + P && 0 >= Q] 17. f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && D1 >= 1 && J >= 1 + C] 18. f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + D1 && J >= 1 + C] 19. f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + C] 20. f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && J >= 1 + E] 21. f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,2 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && E >= J] 22. f49(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f54(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 23. f54(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f60(B,C,D,E,H,J,L,N,O,P,Q,C + Q) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 24. f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L >= 1] 25. f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + L] 26. f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,0,N,O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L = 0] 27. f60(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*A1 + C >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] 28. f91(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(A + B,C,D,E,H,J,L,N,1 + O,P,Q,A1) [D + -1*H >= 0 (?,1) && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + D] Signature: {(f0,27) ;(f117,27) ;(f125,27) ;(f23,27) ;(f33,27) ;(f39,27) ;(f44,27) ;(f46,27) ;(f49,27) ;(f54,27) ;(f60,27) ;(f66,27) ;(f72,27) ;(f87,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28},27->{13 ,14,15,16},28->{9,10}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f0(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(0,2*D,D,4*D,D,J,L,N,O,P,Q,A1) True f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + C] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && 0 >= C1 && C >= J] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C1 >= 2 && C >= J] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C >= J] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D && P = 0] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && P >= 1 && J >= 1 + D] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && 0 >= 1 + P && J >= 1 + D] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,1 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && D >= J] f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f117(B1,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && O >= 1 + N] f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N >= O] f39(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D] f117(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f125(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + -1*N + O >= 0 && J >= 1 + D] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f72(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && Q >= 1] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= Q && P = 0] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && P >= 1 && 0 >= Q] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= 1 + P && 0 >= Q] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && D1 >= 1 && J >= 1 + C] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + D1 && J >= 1 + C] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + C] f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && J >= 1 + E] f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,2 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && E >= J] f49(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f54(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f54(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f60(B,C,D,E,H,J,L,N,O,P,Q,C + Q) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L >= 1] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + L] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L = 0] f60(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*A1 + C >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f91(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(A + B,C,D,E,H,J,L,N,1 + O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + D] Signature: {(f0,27) ;(f117,27) ;(f125,27) ;(f23,27) ;(f33,27) ;(f39,27) ;(f44,27) ;(f46,27) ;(f49,27) ;(f54,27) ;(f60,27) ;(f66,27) ;(f72,27) ;(f87,27) ;(f91,27)} Rule Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28},27->{13 ,14,15,16},28->{9,10}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f0(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(0,2*D,D,4*D,D,J,L,N,O,P,Q,A1) True f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + C] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && 0 >= C1 && C >= J] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C1 >= 2 && C >= J] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C >= J] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D && P = 0] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && P >= 1 && J >= 1 + D] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && 0 >= 1 + P && J >= 1 + D] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,1 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && D >= J] f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f117(B1,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && O >= 1 + N] f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N >= O] f39(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D] f117(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f125(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + -1*N + O >= 0 && J >= 1 + D] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f72(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && Q >= 1] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= Q && P = 0] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && P >= 1 && 0 >= Q] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= 1 + P && 0 >= Q] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && D1 >= 1 && J >= 1 + C] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + D1 && J >= 1 + C] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + C] f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && J >= 1 + E] f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,2 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && E >= J] f49(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f54(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f54(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f60(B,C,D,E,H,J,L,N,O,P,Q,C + Q) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L >= 1] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + L] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L = 0] f60(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*A1 + C >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f91(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(A + B,C,D,E,H,J,L,N,1 + O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f125(B,C,D,E,H,J,L,N,O,P,Q,A1) -> exitus616(B,C,D,E,H,J,L,N,O,P,Q,A1) True f125(B,C,D,E,H,J,L,N,O,P,Q,A1) -> exitus616(B,C,D,E,H,J,L,N,O,P,Q,A1) True f125(B,C,D,E,H,J,L,N,O,P,Q,A1) -> exitus616(B,C,D,E,H,J,L,N,O,P,Q,A1) True Signature: {(exitus616,12) ;(f0,27) ;(f117,27) ;(f125,27) ;(f23,27) ;(f33,27) ;(f39,27) ;(f44,27) ;(f46,27) ;(f49,27) ;(f54,27) ;(f60,27) ;(f66,27) ;(f72,27) ;(f87,27) ;(f91,27)} Rule Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{29,30,31},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25 ,26},18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10}] + 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] | +- p:[2,3,4] c: [2,3,4] | +- p:[8] c: [8] | `- p:[10,28,24,17,13,20,14,27,23,22,15,16,21,18,19,25,26] c: [10,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f0(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(0,2*D,D,4*D,D,J,L,N,O,P,Q,A1) True f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + C] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && 0 >= C1 && C >= J] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,1 + -1*C1,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C1 >= 2 && C >= J] f23(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f23(B,C,D,E,H,1 + J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1*B >= 0 && B >= 0 && C >= J] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D && P = 0] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && P >= 1 && J >= 1 + D] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f39(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && 0 >= 1 + P && J >= 1 + D] f33(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f33(B,C,D,E,H,1 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1*D + H >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && D >= J] f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f117(B1,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && O >= 1 + N] f44(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N >= O] f39(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*B >= 0 && B >= 0 && J >= 1 + D] f117(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f125(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + -1*N + O >= 0 && J >= 1 + D] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f72(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && Q >= 1] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,J,L,N,O,0,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= Q && P = 0] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && P >= 1 && 0 >= Q] f46(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f49(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && N + -1*O >= 0 && 0 >= 1 + P && 0 >= Q] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && D1 >= 1 && J >= 1 + C] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + D1 && J >= 1 + C] f72(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f87(B,C,D,E,H,J,B1,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + C] f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && J >= 1 + E] f66(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f66(B,C,D,E,H,2 + J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && E >= J] f49(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f54(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f54(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f60(B,C,D,E,H,J,L,N,O,P,Q,C + Q) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L >= 1] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,L,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && 0 >= 1 + L] f87(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f91(B,C,D,E,H,J,0,N,O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && L = 0] f60(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f46(B,C,D,E,H,J,L,N,O,P,1 + Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1*A1 + C >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f91(B,C,D,E,H,J,L,N,O,P,Q,A1) -> f44(A + B,C,D,E,H,J,L,N,1 + O,P,Q,A1) [D + -1*H >= 0 && -1 + -1*H + J >= 0 && -1*D + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*C + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && J >= 1 + D] f125(B,C,D,E,H,J,L,N,O,P,Q,A1) -> exitus616(B,C,D,E,H,J,L,N,O,P,Q,A1) True f125(B,C,D,E,H,J,L,N,O,P,Q,A1) -> exitus616(B,C,D,E,H,J,L,N,O,P,Q,A1) True f125(B,C,D,E,H,J,L,N,O,P,Q,A1) -> exitus616(B,C,D,E,H,J,L,N,O,P,Q,A1) True Signature: {(exitus616,12) ;(f0,27) ;(f117,27) ;(f125,27) ;(f23,27) ;(f33,27) ;(f39,27) ;(f44,27) ;(f46,27) ;(f49,27) ;(f54,27) ;(f60,27) ;(f66,27) ;(f72,27) ;(f87,27) ;(f91,27)} Rule Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{29,30,31},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25 ,26},18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10}] ,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] | +- p:[2,3,4] c: [2,3,4] | +- p:[8] c: [8] | `- p:[10,28,24,17,13,20,14,27,23,22,15,16,21,18,19,25,26] c: [10,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [B,C,D,E,H,J,L,N,O,P,Q,A1,0.0,0.1,0.2] f0 ~> f23 [B <= 0*K, C <= 2*D, D <= D, E <= 4*D, H <= D, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f23 ~> f33 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f23 ~> f23 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f23 ~> f23 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f23 ~> f23 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= 0*K, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f33 ~> f44 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= 0*K, Q <= Q, A1 <= A1] f33 ~> f39 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f33 ~> f39 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f33 ~> f33 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f44 ~> f117 [B <= unknown, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f44 ~> f46 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f39 ~> f44 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f117 ~> f125 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f46 ~> f72 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f46 ~> f66 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= 0*K, Q <= Q, A1 <= A1] f46 ~> f49 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f46 ~> f49 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f72 ~> f87 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f72 ~> f87 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f72 ~> f87 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f66 ~> f46 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= K + Q, A1 <= A1] f66 ~> f66 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= 2*K + J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f49 ~> f54 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f54 ~> f60 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= C + Q] f87 ~> f91 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f87 ~> f91 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f87 ~> f91 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= 0*K, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f60 ~> f46 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= K + Q, A1 <= A1] f91 ~> f44 [B <= unknown, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= K + O, P <= P, Q <= Q, A1 <= A1] f125 ~> exitus616 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f125 ~> exitus616 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f125 ~> exitus616 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] + Loop: [0.0 <= C + J] f23 ~> f23 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f23 ~> f23 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f23 ~> f23 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= 0*K, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] + Loop: [0.1 <= D + J] f33 ~> f33 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= K + J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] + Loop: [0.2 <= K + C + 8*E + 6*H + J + N + O + Q] f44 ~> f46 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f91 ~> f44 [B <= unknown, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= K + O, P <= P, Q <= Q, A1 <= A1] f87 ~> f91 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f72 ~> f87 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f46 ~> f72 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f66 ~> f46 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= K + Q, A1 <= A1] f46 ~> f66 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= 0*K, Q <= Q, A1 <= A1] f60 ~> f46 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= K + Q, A1 <= A1] f54 ~> f60 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= C + Q] f49 ~> f54 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f46 ~> f49 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f46 ~> f49 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f66 ~> f66 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= 2*K + J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f72 ~> f87 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f72 ~> f87 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= unknown, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f87 ~> f91 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= L, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] f87 ~> f91 [B <= B, C <= C, D <= D, E <= E, H <= H, J <= J, L <= 0*K, N <= N, O <= O, P <= P, Q <= Q, A1 <= A1] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,B,C,D,E,H,J,L,N,O,P,Q,A1,0.0,0.1,0.2] f0 ~> f23 [D ~=> H,K ~=> B,D ~*> C,D ~*> E] f23 ~> f33 [] f23 ~> f23 [huge ~=> L,J ~+> J,K ~+> J] f23 ~> f23 [huge ~=> L,J ~+> J,K ~+> J] f23 ~> f23 [K ~=> L,J ~+> J,K ~+> J] f33 ~> f44 [K ~=> P] f33 ~> f39 [] f33 ~> f39 [] f33 ~> f33 [J ~+> J,K ~+> J] f44 ~> f117 [huge ~=> B] f44 ~> f46 [] f39 ~> f44 [] f117 ~> f125 [] f46 ~> f72 [] f46 ~> f66 [K ~=> P] f46 ~> f49 [] f46 ~> f49 [] f72 ~> f87 [huge ~=> L] f72 ~> f87 [huge ~=> L] f72 ~> f87 [huge ~=> L] f66 ~> f46 [Q ~+> Q,K ~+> Q] f66 ~> f66 [J ~+> J,K ~*> J] f49 ~> f54 [] f54 ~> f60 [C ~+> A1,Q ~+> A1] f87 ~> f91 [] f87 ~> f91 [] f87 ~> f91 [K ~=> L] f60 ~> f46 [Q ~+> Q,K ~+> Q] f91 ~> f44 [huge ~=> B,O ~+> O,K ~+> O] f125 ~> exitus616 [] f125 ~> exitus616 [] f125 ~> exitus616 [] + Loop: [C ~+> 0.0,J ~+> 0.0] f23 ~> f23 [huge ~=> L,J ~+> J,K ~+> J] f23 ~> f23 [huge ~=> L,J ~+> J,K ~+> J] f23 ~> f23 [K ~=> L,J ~+> J,K ~+> J] + Loop: [D ~+> 0.1,J ~+> 0.1] f33 ~> f33 [J ~+> J,K ~+> J] + Loop: [C ~+> 0.2,J ~+> 0.2,N ~+> 0.2,O ~+> 0.2,Q ~+> 0.2,K ~+> 0.2,E ~*> 0.2,H ~*> 0.2] f44 ~> f46 [] f91 ~> f44 [huge ~=> B,O ~+> O,K ~+> O] f87 ~> f91 [] f72 ~> f87 [huge ~=> L] f46 ~> f72 [] f66 ~> f46 [Q ~+> Q,K ~+> Q] f46 ~> f66 [K ~=> P] f60 ~> f46 [Q ~+> Q,K ~+> Q] f54 ~> f60 [C ~+> A1,Q ~+> A1] f49 ~> f54 [] f46 ~> f49 [] f46 ~> f49 [] f66 ~> f66 [J ~+> J,K ~*> J] f72 ~> f87 [huge ~=> L] f72 ~> f87 [huge ~=> L] f87 ~> f91 [] f87 ~> f91 [K ~=> L] + Applied Processor: Lare + Details: f0 ~> exitus616 [D ~=> H ,K ~=> L ,K ~=> P ,huge ~=> B ,huge ~=> L ,D ~+> 0.1 ,D ~+> tick ,J ~+> J ,J ~+> 0.0 ,J ~+> 0.1 ,J ~+> 0.2 ,J ~+> tick ,N ~+> 0.2 ,N ~+> tick ,O ~+> O ,O ~+> 0.2 ,O ~+> tick ,Q ~+> A1 ,Q ~+> Q ,Q ~+> 0.2 ,Q ~+> tick ,tick ~+> tick ,K ~+> A1 ,K ~+> J ,K ~+> O ,K ~+> Q ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> tick ,D ~*> A1 ,D ~*> C ,D ~*> E ,D ~*> J ,D ~*> O ,D ~*> Q ,D ~*> 0.0 ,D ~*> 0.1 ,D ~*> 0.2 ,D ~*> tick ,J ~*> A1 ,J ~*> J ,J ~*> O ,J ~*> Q ,J ~*> 0.1 ,J ~*> 0.2 ,J ~*> tick ,N ~*> A1 ,N ~*> J ,N ~*> O ,N ~*> Q ,O ~*> A1 ,O ~*> J ,O ~*> O ,O ~*> Q ,Q ~*> A1 ,Q ~*> J ,Q ~*> O ,Q ~*> Q ,K ~*> A1 ,K ~*> J ,K ~*> O ,K ~*> Q ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> tick] + f23> [K ~=> L ,huge ~=> L ,C ~+> 0.0 ,C ~+> tick ,J ~+> J ,J ~+> 0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,C ~*> J ,J ~*> J ,K ~*> J] + f33> [D ~+> 0.1 ,D ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,D ~*> J ,J ~*> J ,K ~*> J] + f44> [K ~=> L ,K ~=> P ,huge ~=> B ,huge ~=> L ,C ~+> A1 ,C ~+> 0.2 ,C ~+> tick ,J ~+> J ,J ~+> 0.2 ,J ~+> tick ,N ~+> 0.2 ,N ~+> tick ,O ~+> O ,O ~+> 0.2 ,O ~+> tick ,Q ~+> A1 ,Q ~+> Q ,Q ~+> 0.2 ,Q ~+> tick ,tick ~+> tick ,K ~+> A1 ,K ~+> O ,K ~+> Q ,K ~+> 0.2 ,K ~+> tick ,C ~*> A1 ,C ~*> J ,C ~*> O ,C ~*> Q ,E ~*> A1 ,E ~*> J ,E ~*> O ,E ~*> Q ,E ~*> 0.2 ,E ~*> tick ,H ~*> A1 ,H ~*> J ,H ~*> O ,H ~*> Q ,H ~*> 0.2 ,H ~*> tick ,J ~*> A1 ,J ~*> J ,J ~*> O ,J ~*> Q ,N ~*> A1 ,N ~*> J ,N ~*> O ,N ~*> Q ,O ~*> A1 ,O ~*> J ,O ~*> O ,O ~*> Q ,Q ~*> A1 ,Q ~*> J ,Q ~*> O ,Q ~*> Q ,K ~*> A1 ,K ~*> J ,K ~*> O ,K ~*> Q] YES(?,POLY)