YES(?,O(n^1)) * Step 1: ArgumentFilter 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) -> f13(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H >= I] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [J >= K] (?,1) 3. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f27(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f27(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= Q && J >= K] (?,1) 10. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [Q >= 2 && J >= K] (?,1) 11. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f38(A,B,C,D,E,F,G,H,I,J,1 + K,3 + X,M,N,O,P,1,B*Y + B*Z,A1*B + -1*B*B1,C*C1 + -1*C*D1,-1*C*E1 + -1*C*F1[J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) ,V,W) 12. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f38(A,B,C,D,E,F,G,H,I,J,1 + K,3 + X,M,N,O,P,1,B*Y + B*Z,A1*B + -1*B*B1,C*C1 + -1*C*D1,-1*C*E1 + -1*C*F1[J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) ,V,W) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f38(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,B*X + B*Y,-1*A1*B + B*Z,B1*C + -1*C*C1,-1*C*D1 + -1*C*E1,V,W) [J >= 1 && K = 1 && Q = 1] (?,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) -> f38(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,B*X + B*Y,-1*A1*B + B*Z,B1*C + -1*C*C1 [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) ,-1*C*D1 + -1*C*E1,3 + -1*F1 + P,W) 15. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f38(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,B*X + B*Y,-1*A1*B + B*Z,B1*C + -1*C*C1 [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) ,-1*C*D1 + -1*C*E1,3 + -1*F1 + P,W) 16. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f38(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,B*X + B*Y,-1*A1*B + B*Z,B1*C + -1*C*C1,-1*C*D1 + -1*C*E1 [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) ,3 + -1*F1 + P,W) 17. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,F*N + -1*G*O + N,F*O + G*N + O,P,1 + Q,R,S,T,U,V,2 + W) [K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f27(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f1(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f13(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [K >= 1 + J] (?,1) 23. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H] (?,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,19,20,21},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{9,10,11,12,13,17},12->{9,10,11,12,13,17},13->{9,10,11,12 ,13,17},14->{9,10,11,12,13,17},15->{9,10,11,12,13,17},16->{9,10,11,12,13,17},17->{8,18},18->{5,6,7,19,20,21} ,19->{},20->{},21->{},22->{1,23},23->{5,6,7,19,20,21}] + Applied Processor: ArgumentFilter [1,2,3,4,5,6,11,12,13,14,17,18,19,20,21,22] + Details: We remove following argument positions: [1,2,3,4,5,6,11,12,13,14,17,18,19,20,21,22]. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (?,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (?,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (?,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (?,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (?,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (?,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (?,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (?,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,19,20,21},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{9,10,11,12,13,17},12->{9,10,11,12,13,17},13->{9,10,11,12 ,13,17},14->{9,10,11,12,13,17},15->{9,10,11,12,13,17},16->{9,10,11,12,13,17},17->{8,18},18->{5,6,7,19,20,21} ,19->{},20->{},21->{},22->{1,23},23->{5,6,7,19,20,21}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,19) ,(4,21) ,(9,14) ,(9,15) ,(9,16) ,(11,9) ,(11,10) ,(11,12) ,(11,17) ,(12,9) ,(12,10) ,(12,11) ,(12,13) ,(12,17) ,(13,9) ,(13,10) ,(13,11) ,(13,13) ,(14,9) ,(14,11) ,(14,12) ,(14,13) ,(15,9) ,(15,11) ,(15,12) ,(15,13) ,(16,9) ,(16,11) ,(16,12) ,(16,13) ,(23,5) ,(23,6) ,(23,7)] * Step 3: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (?,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (?,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (?,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (?,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (?,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (?,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (?,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (?,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (?,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (?,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (?,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (?,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x2 + -1*x3 + x23 p(f13) = x2 + -1*x3 + x23 p(f16) = x2 + -1*x3 p(f2) = x2 + -1*x3 + x23 p(f27) = x2 + -1*x3 + x23 p(f35) = x2 + -1*x3 + x23 p(f38) = x2 + -1*x3 + x23 p(f53) = x2 + -1*x3 + x23 Following rules are strictly oriented: [H >= I] ==> f13(A,H,I,J,K,P,Q) = 1 + H + -1*I > H + -1*I = f16(A,H,I,J,K,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f13(1,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = H + -1*I >= H + -1*I = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 1 + H + -1*I >= H = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= H + -1*I = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = H + -1*I >= H + -1*I = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f27(A,H,I,J,K,P,Q) * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (?,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (?,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (?,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x2 + -1*x3 + 2*x23 p(f13) = x2 + -1*x3 + 2*x23 p(f16) = x2 + -1*x3 + x23 p(f2) = x2 + -1*x3 + 2*x23 p(f27) = x2 + -1*x3 + 2*x23 p(f35) = x2 + -1*x3 + x23 p(f38) = x2 + -1*x3 + x23 p(f53) = x2 + -1*x3 + x23 Following rules are strictly oriented: [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + H + -1*I > 1 + H + -1*I = f16(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I > H = f35(A,H,1,J,K,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f13(1,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (?,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (?,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x2 + -1*x3 + 2*x23 p(f13) = x2 + -1*x3 + 2*x23 p(f16) = x2 + -1*x3 + x23 p(f2) = x2 + -1*x3 + 2*x23 p(f27) = x2 + -1*x3 + 2*x23 p(f35) = x2 + -1*x3 + x23 p(f38) = x2 + -1*x3 + x23 p(f53) = x2 + -1*x3 + x23 Following rules are strictly oriented: [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + H + -1*I > 1 + H + -1*I = f16(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I > 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I > H = f35(A,H,1,J,K,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f13(1,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) * Step 7: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (?,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x2 + -1*x3 + 2*x23 p(f13) = x2 + -1*x3 + 2*x23 p(f16) = x2 + -1*x3 + x23 p(f2) = x2 + -1*x3 + 2*x23 p(f27) = x2 + -1*x3 + 2*x23 p(f35) = x2 + -1*x3 + x23 p(f38) = x2 + -1*x3 + x23 p(f53) = x2 + -1*x3 + x23 Following rules are strictly oriented: [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + H + -1*I > 1 + H + -1*I = f16(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I > 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I > 1 + H + -1*I = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I > H = f35(A,H,1,J,K,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f13(1,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + H + -1*I >= 1 + H + -1*I = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + H + -1*I >= 2 + H + -1*I = f27(A,H,I,J,K,P,Q) * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x6 + -1*x7 + x23 p(f13) = x6 + -1*x7 + x23 p(f16) = x6 + -1*x7 + x23 p(f2) = x6 + -1*x7 + x23 p(f27) = x6 + -1*x7 + x23 p(f35) = x6 + -1*x7 + x23 p(f38) = x6 + -1*x7 p(f53) = x6 + -1*x7 Following rules are strictly oriented: [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + P + -1*Q > P + -1*Q = f38(A,H,I,J,K,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f16(A,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f35(A,H,1,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = P + -1*Q >= P + -1*Q = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = P + -1*Q >= P + -1*Q = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = P + -1*Q >= -1 + P = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = P + -1*Q >= -1 + P = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = P + -1*Q >= -1 + P = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = P + -1*Q >= P + -1*Q = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = P + -1*Q >= P + -1*Q = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = P + -1*Q >= P + -1*Q = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = P + -1*Q >= P + -1*Q = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 1 + P + -1*Q >= 1 + P + -1*Q = f27(A,H,I,J,K,P,Q) * Step 9: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (?,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = -1*x5 + 2*x23 p(f13) = -1*x5 + 2*x23 p(f16) = -1*x5 + 2*x23 p(f2) = -1*x5 + 2*x23 p(f27) = -1*x5 + 2*x23 p(f35) = -1*x5 + 2*x23 p(f38) = -1*x5 + 2*x23 p(f53) = -1*x5 + 2*x23 Following rules are strictly oriented: [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 2 + -1*K > 0 = f38(A,H,I,J,2,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f16(A,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 0 = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) * Step 10: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (?,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = -1*x5 + 2*x23 p(f13) = -1*x5 + 2*x23 p(f16) = -1*x5 + 2*x23 p(f2) = -1*x5 + 2*x23 p(f27) = -1*x5 + 2*x23 p(f35) = -1*x5 + 2*x23 p(f38) = -1*x5 + 2*x23 p(f53) = -1*x5 + x23 Following rules are strictly oriented: [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K > 0 = f38(A,H,I,J,2,P,1) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f16(A,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 1 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 1 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 1 + -1*K >= 0 = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) * Step 11: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (?,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x4 + -1*x5 + x23 p(f13) = x4 + -1*x5 + x23 p(f16) = x4 + -1*x5 + x23 p(f2) = x4 + -1*x5 + x23 p(f27) = x4 + -1*x5 + x23 p(f35) = x4 + -1*x5 + x23 p(f38) = x4 + -1*x5 + x23 p(f53) = x4 + -1*x5 Following rules are strictly oriented: [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > -1 + J = f38(A,H,I,J,2,P,1) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f16(A,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + J + -1*K >= J + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f38(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K >= J + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= -1 + J = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) * Step 12: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (?,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = -1*x5 + 2*x23 p(f13) = -1*x5 + 2*x23 p(f16) = -1*x5 + 2*x23 p(f2) = -1*x5 + 2*x23 p(f27) = -1*x5 + 2*x23 p(f35) = -1*x5 + 2*x23 p(f38) = -1*x5 + 2*x23 p(f53) = -1*x5 + x23 Following rules are strictly oriented: [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K > 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K > 0 = f38(A,H,I,J,2,P,1) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f16(A,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 1 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 1 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 1 + -1*K >= 0 = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) * Step 13: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (2 + K,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (?,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = -1*x5 + 2*x23 p(f13) = -1*x5 + 2*x23 p(f16) = -1*x5 + 2*x23 p(f2) = -1*x5 + 2*x23 p(f27) = -1*x5 + 2*x23 p(f35) = -1*x5 + 2*x23 p(f38) = -1*x5 + 2*x23 p(f53) = -1*x5 + 2*x23 Following rules are strictly oriented: [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K > 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K > 0 = f38(A,H,I,J,2,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = 2 + -1*K > 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = 2 + -1*K > 0 = f38(A,H,I,J,2,P,Q) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f16(A,H,I,J,K,P,Q) [J >= K] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f38(A,H,I,J,K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,1) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = 2 + -1*K >= 1 + -1*K = f38(A,H,I,J,1 + K,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 2 + -1*K >= 2 + -1*K = f27(A,H,I,J,K,P,Q) * Step 14: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (?,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (2 + K,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (2 + K,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x4 + -1*x5 + x23 p(f13) = x4 + -1*x5 + x23 p(f16) = x4 + -1*x5 + x23 p(f2) = x4 + -1*x5 + x23 p(f27) = x4 + -1*x5 + x23 p(f35) = x4 + -1*x5 + x23 p(f38) = x4 + -1*x5 + x23 p(f53) = x4 + -1*x5 Following rules are strictly oriented: [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > -1 + J = f38(A,H,I,J,2,P,1) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f16(A,H,I,J,K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f38(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K >= J + -1*K = f53(A,H,I,J,K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= -1 + J = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) * Step 15: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (1 + J + K,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (2 + K,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (2 + K,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 16: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (1 + J + K,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (2 + K,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (2 + K,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (2 + H + I + J + K,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = x4 + -1*x5 + x23 p(f13) = x4 + -1*x5 + x23 p(f16) = x4 + -1*x5 + x23 p(f2) = x4 + -1*x5 + x23 p(f27) = x4 + -1*x5 + x23 p(f35) = x4 + -1*x5 + x23 p(f38) = x4 + -1*x5 + x23 p(f53) = x4 + -1*x5 Following rules are strictly oriented: [J >= K] ==> f16(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f16(A,H,I,J,1 + K,P,Q) [0 >= Q && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f53(A,H,I,J,K,P,Q) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > J + -1*K = f38(A,H,I,J,1 + K,P,1) [J >= 1 && K = 1 && Q = 1] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K > -1 + J = f38(A,H,I,J,2,P,1) Following rules are weakly oriented: [A = 1] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f13(1,H,I,J,K,P,Q) [H >= I] ==> f13(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f16(A,H,I,J,K,P,Q) [0 >= A] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) [A >= 2] ==> f2(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) [0 >= I && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,Q) [H >= 1 && I = 1] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,1,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] ==> f35(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f38(A,H,I,J,K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= J + -1*K = f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] ==> f53(A,H,I,J,K,P,Q) = J + -1*K >= -1 + J = f38(A,H,I,J,2,P,Q) [K >= 1 + J] ==> f38(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f35(A,H,I,J,K,P,1 + Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] ==> f35(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,1 + I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(A,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] ==> f27(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f1(-1,H,I,J,K,P,Q) [K >= 1 + J] ==> f16(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f13(A,H,1 + I,J,K,P,Q) [I >= 1 + H] ==> f13(A,H,I,J,K,P,Q) = 1 + J + -1*K >= 1 + J + -1*K = f27(A,H,I,J,K,P,Q) * Step 17: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (1 + J + K,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (1 + J + K,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (2 + K,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (2 + K,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (?,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (2 + H + I + J + K,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 18: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] (1,1) 1. f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [H >= I] (1 + H + I,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [J >= K] (1 + J + K,1) 3. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] (1,1) 4. f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] (1,1) 5. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] (2 + H + I,1) 6. f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] (2 + H + I,1) 7. f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] (2 + H + I,1) 8. f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (1 + P + Q,1) 9. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [0 >= Q && J >= K] (1,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [Q >= 2 && J >= K] (1 + J + K,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] (2 + K,1) 12. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] (1 + J + K,1) 13. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [J >= 1 && K = 1 && Q = 1] (2 + K,1) 14. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] (2 + K,1) 15. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] (1 + J + K,1) 16. f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] (2 + K,1) 17. f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [K >= 1 + J] (8 + J + 4*K + P + Q,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (14 + 3*H + 3*I + J + 4*K + P + Q,1) 19. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] (1,1) 21. f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] (1,1) 22. f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [K >= 1 + J] (2 + H + I + J + K,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [I >= 1 + H] (1,1) Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{},10->{14,15,16},11->{11,13},12->{12},13->{12,17},14->{10,17},15->{10,17},16->{10,17},17->{8 ,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{19,20,21}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))