YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(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) -> f2(A,1 + B,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) [A >= B] (?,1) 1. 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,Y,Z,A1) -> f19(A,B,C,D,B1,Q1,D1,G1,L1,1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= 2*C1 (?,1) && 3*C1 >= 1 + D && C1 >= D1 && D >= 2*E1 && 3*E1 >= 1 + D && D1 >= E1 && B1*D >= 2*B1*F1 && 2*B1*F1 + F1 >= 1 + B1*D && F1 >= G1 && B1*D >= 2*B1*H1 && 2*B1*H1 + H1 >= 1 + B1*D && G1 >= H1 && C >= B1*D*I1 && B1*D*I1 + I1 >= 1 + C && C >= B1*D*J1 && B1*D*J1 + J1 >= 1 + C && B1*D*I1 >= 2*B1*J1*K1 && 2*B1*J1*K1 + K1 >= 1 + B1*D*I1 && K1 >= L1 && C >= B1*D*M1 && B1*D*M1 + M1 >= 1 + C && C >= B1*D*N1 && B1*D*N1 + N1 >= 1 + C && B1*D*M1 >= 2*B1*N1*O1 && 2*B1*N1*O1 + O1 >= 1 + B1*D*M1 && L1 >= O1 && B >= 1 && C >= B1*D*P1 && B1*D*P1 + P1 >= 1 + C && P1 >= Q1 && C >= B1*D*R1 && B1*D*R1 + R1 >= 1 + C && Q1 >= R1] 2. f19(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,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= K && J >= 1 + K] (?,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) -> f26(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) [G + K >= 2 + L] (?,1) 4. f26(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) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,H + M,J + -1*K + M,B1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [I >= M] (?,1) 5. f19(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) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [K >= J && H >= 2*Q1 && 3*Q1 >= 1 + H && Q1 >= B1 && H >= 2*D1 && 3*D1 >= 1 + H && B1 >= D1 && H >= K] (?,1) 6. f41(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) -> f41(A,B,C,D,E,F,G,H,I,J + -1*P,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + P && P >= 2*Q1 && 3*Q1 >= 1 + P && Q1 >= B1 && P >= 2*D1 && 3*D1 >= 1 + P && B1 >= D1 && P >= G] (?,1) 7. f53(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,2*Q,B1,Q1,D1,G1,1,0,Y,Z,A1) [H >= 1 + Q] (?,1) 8. f63(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,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= M] (?,1) 9. 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) -> f69(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) [G + M >= 2 + L] (?,1) 10. f69(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) -> f69(A,B,C,D,E,F,G,H,I,J,K + R,L,M,N,B1*W + -1*Q1*X,P,Q,R,S,T,U,V,W,X,K,K + Q,D1*W + G1*X) [I >= K] (?,1) 11. f69(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,2 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [K >= 1 + I] (?,1) 12. 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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,G + M,N,O,P,Q,R,S,W,U,V,U*W + -1*V*X + W,U*X + V*W + X,Y,Z,A1) [1 + L >= G + M] (?,1) 13. f63(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) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,R,R,S,T,U,V,W,X,Y,Z,A1) [M >= 1 + Q] (?,1) 14. f53(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) -> f10(A,-1 + B,C,D*E,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= H] (?,1) 15. f41(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) -> f19(A,B,C,D,E,F,G,H,I,J + P,G + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= G && P >= J] (?,1) 16. f41(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) -> f19(A,B,C,D,E,F,G,H,I,J + P,G + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [G >= 1 + P] (?,1) 17. f26(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,J,K,2 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [M >= 1 + I] (?,1) 18. 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) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 + L >= G + K && H >= 2*Q1 && 3*Q1 >= 1 + H && Q1 >= B1 && H >= 2*D1 && 3*D1 >= 1 + H && B1 >= D1] (?,1) 19. f19(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) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,G,R,S,T,U,V,W,X,Y,Z,A1) [K >= 1 + H] (?,1) 20. 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,Y,Z,A1) -> 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,Y,Z,A1) [0 >= B] (?,1) 21. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 22. start(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) -> f2(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) True (1,1) Signature: {(f1,27) ;(f10,27) ;(f19,27) ;(f2,27) ;(f23,27) ;(f26,27) ;(f41,27) ;(f53,27) ;(f63,27) ;(f66,27) ;(f69,27) ;(start,27)} Flow Graph: [0->{0,21},1->{2,5,19},2->{3,18},3->{4,17},4->{4,17},5->{6,15,16},6->{6,15,16},7->{8,13},8->{9,12},9->{10 ,11},10->{10,11},11->{9,12},12->{8,13},13->{7,14},14->{1,20},15->{2,5,19},16->{2,5,19},17->{3,18},18->{6,15 ,16},19->{7,14},20->{},21->{1,20},22->{0,21}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(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) -> f2(A,1 + B,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) [A >= B] (?,1) 1. 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,Y,Z,A1) -> f19(A,B,C,D,B1,Q1,D1,G1,L1,1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= 2*C1 (?,1) && 3*C1 >= 1 + D && C1 >= D1 && D >= 2*E1 && 3*E1 >= 1 + D && D1 >= E1 && B1*D >= 2*B1*F1 && 2*B1*F1 + F1 >= 1 + B1*D && F1 >= G1 && B1*D >= 2*B1*H1 && 2*B1*H1 + H1 >= 1 + B1*D && G1 >= H1 && C >= B1*D*I1 && B1*D*I1 + I1 >= 1 + C && C >= B1*D*J1 && B1*D*J1 + J1 >= 1 + C && B1*D*I1 >= 2*B1*J1*K1 && 2*B1*J1*K1 + K1 >= 1 + B1*D*I1 && K1 >= L1 && C >= B1*D*M1 && B1*D*M1 + M1 >= 1 + C && C >= B1*D*N1 && B1*D*N1 + N1 >= 1 + C && B1*D*M1 >= 2*B1*N1*O1 && 2*B1*N1*O1 + O1 >= 1 + B1*D*M1 && L1 >= O1 && B >= 1 && C >= B1*D*P1 && B1*D*P1 + P1 >= 1 + C && P1 >= Q1 && C >= B1*D*R1 && B1*D*R1 + R1 >= 1 + C && Q1 >= R1] 2. f19(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,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= K && J >= 1 + K] (?,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) -> f26(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) [G + K >= 2 + L] (?,1) 4. f26(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) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,H + M,J + -1*K + M,B1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [I >= M] (?,1) 5. f19(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) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [K >= J && H >= 2*Q1 && 3*Q1 >= 1 + H && Q1 >= B1 && H >= 2*D1 && 3*D1 >= 1 + H && B1 >= D1 && H >= K] (?,1) 6. f41(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) -> f41(A,B,C,D,E,F,G,H,I,J + -1*P,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + P && P >= 2*Q1 && 3*Q1 >= 1 + P && Q1 >= B1 && P >= 2*D1 && 3*D1 >= 1 + P && B1 >= D1 && P >= G] (?,1) 7. f53(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,2*Q,B1,Q1,D1,G1,1,0,Y,Z,A1) [H >= 1 + Q] (?,1) 8. f63(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,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= M] (?,1) 9. 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) -> f69(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) [G + M >= 2 + L] (?,1) 10. f69(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) -> f69(A,B,C,D,E,F,G,H,I,J,K + R,L,M,N,B1*W + -1*Q1*X,P,Q,R,S,T,U,V,W,X,K,K + Q,D1*W + G1*X) [I >= K] (?,1) 11. f69(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,2 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [K >= 1 + I] (?,1) 12. 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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,G + M,N,O,P,Q,R,S,W,U,V,U*W + -1*V*X + W,U*X + V*W + X,Y,Z,A1) [1 + L >= G + M] (?,1) 13. f63(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) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,R,R,S,T,U,V,W,X,Y,Z,A1) [M >= 1 + Q] (?,1) 14. f53(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) -> f10(A,-1 + B,C,D*E,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= H] (?,1) 15. f41(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) -> f19(A,B,C,D,E,F,G,H,I,J + P,G + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= G && P >= J] (?,1) 16. f41(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) -> f19(A,B,C,D,E,F,G,H,I,J + P,G + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [G >= 1 + P] (?,1) 17. f26(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,J,K,2 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [M >= 1 + I] (?,1) 18. 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) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 + L >= G + K && H >= 2*Q1 && 3*Q1 >= 1 + H && Q1 >= B1 && H >= 2*D1 && 3*D1 >= 1 + H && B1 >= D1] (?,1) 19. f19(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) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,G,R,S,T,U,V,W,X,Y,Z,A1) [K >= 1 + H] (?,1) 20. 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,Y,Z,A1) -> 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,Y,Z,A1) [0 >= B] (1,1) 21. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (1,1) 22. start(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) -> f2(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) True (1,1) Signature: {(f1,27) ;(f10,27) ;(f19,27) ;(f2,27) ;(f23,27) ;(f26,27) ;(f41,27) ;(f53,27) ;(f63,27) ;(f66,27) ;(f69,27) ;(start,27)} Flow Graph: [0->{0,21},1->{2,5,19},2->{3,18},3->{4,17},4->{4,17},5->{6,15,16},6->{6,15,16},7->{8,13},8->{9,12},9->{10 ,11},10->{10,11},11->{9,12},12->{8,13},13->{7,14},14->{1,20},15->{2,5,19},16->{2,5,19},17->{3,18},18->{6,15 ,16},19->{7,14},20->{},21->{1,20},22->{0,21}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(21,1)] * Step 3: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(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) -> f2(A,1 + B,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) [A >= B] (?,1) 1. 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,Y,Z,A1) -> f19(A,B,C,D,B1,Q1,D1,G1,L1,1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= 2*C1 (?,1) && 3*C1 >= 1 + D && C1 >= D1 && D >= 2*E1 && 3*E1 >= 1 + D && D1 >= E1 && B1*D >= 2*B1*F1 && 2*B1*F1 + F1 >= 1 + B1*D && F1 >= G1 && B1*D >= 2*B1*H1 && 2*B1*H1 + H1 >= 1 + B1*D && G1 >= H1 && C >= B1*D*I1 && B1*D*I1 + I1 >= 1 + C && C >= B1*D*J1 && B1*D*J1 + J1 >= 1 + C && B1*D*I1 >= 2*B1*J1*K1 && 2*B1*J1*K1 + K1 >= 1 + B1*D*I1 && K1 >= L1 && C >= B1*D*M1 && B1*D*M1 + M1 >= 1 + C && C >= B1*D*N1 && B1*D*N1 + N1 >= 1 + C && B1*D*M1 >= 2*B1*N1*O1 && 2*B1*N1*O1 + O1 >= 1 + B1*D*M1 && L1 >= O1 && B >= 1 && C >= B1*D*P1 && B1*D*P1 + P1 >= 1 + C && P1 >= Q1 && C >= B1*D*R1 && B1*D*R1 + R1 >= 1 + C && Q1 >= R1] 2. f19(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,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= K && J >= 1 + K] (?,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) -> f26(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) [G + K >= 2 + L] (?,1) 4. f26(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) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,H + M,J + -1*K + M,B1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [I >= M] (?,1) 5. f19(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) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [K >= J && H >= 2*Q1 && 3*Q1 >= 1 + H && Q1 >= B1 && H >= 2*D1 && 3*D1 >= 1 + H && B1 >= D1 && H >= K] (?,1) 6. f41(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) -> f41(A,B,C,D,E,F,G,H,I,J + -1*P,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + P && P >= 2*Q1 && 3*Q1 >= 1 + P && Q1 >= B1 && P >= 2*D1 && 3*D1 >= 1 + P && B1 >= D1 && P >= G] (?,1) 7. f53(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,2*Q,B1,Q1,D1,G1,1,0,Y,Z,A1) [H >= 1 + Q] (?,1) 8. f63(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,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= M] (?,1) 9. 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) -> f69(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) [G + M >= 2 + L] (?,1) 10. f69(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) -> f69(A,B,C,D,E,F,G,H,I,J,K + R,L,M,N,B1*W + -1*Q1*X,P,Q,R,S,T,U,V,W,X,K,K + Q,D1*W + G1*X) [I >= K] (?,1) 11. f69(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,2 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [K >= 1 + I] (?,1) 12. 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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,G + M,N,O,P,Q,R,S,W,U,V,U*W + -1*V*X + W,U*X + V*W + X,Y,Z,A1) [1 + L >= G + M] (?,1) 13. f63(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) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,R,R,S,T,U,V,W,X,Y,Z,A1) [M >= 1 + Q] (?,1) 14. f53(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) -> f10(A,-1 + B,C,D*E,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= H] (?,1) 15. f41(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) -> f19(A,B,C,D,E,F,G,H,I,J + P,G + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= G && P >= J] (?,1) 16. f41(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) -> f19(A,B,C,D,E,F,G,H,I,J + P,G + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [G >= 1 + P] (?,1) 17. f26(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,J,K,2 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [M >= 1 + I] (?,1) 18. 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) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 + L >= G + K && H >= 2*Q1 && 3*Q1 >= 1 + H && Q1 >= B1 && H >= 2*D1 && 3*D1 >= 1 + H && B1 >= D1] (?,1) 19. f19(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) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,G,R,S,T,U,V,W,X,Y,Z,A1) [K >= 1 + H] (?,1) 20. 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,Y,Z,A1) -> 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,Y,Z,A1) [0 >= B] (1,1) 21. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (1,1) 22. start(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) -> f2(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) True (1,1) Signature: {(f1,27) ;(f10,27) ;(f19,27) ;(f2,27) ;(f23,27) ;(f26,27) ;(f41,27) ;(f53,27) ;(f63,27) ;(f66,27) ;(f69,27) ;(start,27)} Flow Graph: [0->{0,21},1->{2,5,19},2->{3,18},3->{4,17},4->{4,17},5->{6,15,16},6->{6,15,16},7->{8,13},8->{9,12},9->{10 ,11},10->{10,11},11->{9,12},12->{8,13},13->{7,14},14->{1,20},15->{2,5,19},16->{2,5,19},17->{3,18},18->{6,15 ,16},19->{7,14},20->{},21->{20},22->{0,21}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,14 ,15 ,16 ,17 ,18 ,19] * Step 4: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(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) -> f2(A,1 + B,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) [A >= B] (?,1) 20. 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,Y,Z,A1) -> 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,Y,Z,A1) [0 >= B] (1,1) 21. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (1,1) 22. start(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) -> f2(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) True (1,1) Signature: {(f1,27) ;(f10,27) ;(f19,27) ;(f2,27) ;(f23,27) ;(f26,27) ;(f41,27) ;(f53,27) ;(f63,27) ;(f66,27) ;(f69,27) ;(start,27)} Flow Graph: [0->{0,21},20->{},21->{20},22->{0,21}] + Applied Processor: AddSinks + Details: () * Step 5: LooptreeTransformer WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(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) -> f2(A,1 + B,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) [A >= B] (?,1) 20. 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,Y,Z,A1) -> 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,Y,Z,A1) [0 >= B] (?,1) 21. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 22. start(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) -> f2(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) True (1,1) 23. 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,Y,Z,A1) -> exitus616(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) True (?,1) Signature: {(exitus616,27) ;(f1,27) ;(f10,27) ;(f19,27) ;(f2,27) ;(f23,27) ;(f26,27) ;(f41,27) ;(f53,27) ;(f63,27) ;(f66,27) ;(f69,27) ;(start,27)} Flow Graph: [0->{0,21},20->{},21->{20,23},22->{0,21},23->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,20,21,22,23] | `- p:[0] c: [0] * Step 6: SizeAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: 0. f2(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) -> f2(A,1 + B,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) [A >= B] (?,1) 20. 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,Y,Z,A1) -> 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,Y,Z,A1) [0 >= B] (?,1) 21. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 22. start(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) -> f2(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) True (1,1) 23. 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,Y,Z,A1) -> exitus616(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) True (?,1) Signature: {(exitus616,27) ;(f1,27) ;(f10,27) ;(f19,27) ;(f2,27) ;(f23,27) ;(f26,27) ;(f41,27) ;(f53,27) ;(f63,27) ;(f66,27) ;(f69,27) ;(start,27)} Flow Graph: [0->{0,21},20->{},21->{20,23},22->{0,21},23->{}] ,We construct a looptree: P: [0,20,21,22,23] | `- p:[0] c: [0]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [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,0.0] f2 ~> f2 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f10 ~> f1 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f2 ~> f10 [A <= A, B <= B, C <= C, D <= K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] start ~> f2 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f10 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.0 <= K + A + B] f2 ~> f2 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0.0] f2 ~> f2 [huge ~=> C,B ~+> B,K ~+> B] f10 ~> f1 [] f2 ~> f10 [K ~=> D] start ~> f2 [] f10 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f2 ~> f2 [huge ~=> C,B ~+> B,K ~+> B] + Applied Processor: LareProcessor + Details: start ~> f1 [K ~=> D ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] start ~> exitus616 [K ~=> D ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] + f2> [huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,O(n^1))