YES(?,POLY) * Step 1: ArgumentFilter WORST_CASE(?,POLY) + 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) [1 + -1*A >= 0 && -1 + A >= 0 && 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) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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[H + -1*I >= 0 && 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[H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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 [H + -1*I >= 0 && J + -1*K >= 0 && 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 [H + -1*I >= 0 && J + -1*K >= 0 && 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 [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 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) [1 + -1*A >= 0 && -1 + A >= 0 && 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(?,POLY) + 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) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && 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) ,(23,19) ,(23,21)] * Step 3: FromIts WORST_CASE(?,POLY) + 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) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && J + -1*K >= 0 && 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) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && 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) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && 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->{20}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && 0 >= Q && J >= K] f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && Q >= 2 && J >= K] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [H + -1*I >= 0 && K >= 1 + J] f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] Signature: {(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Rule 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->{20}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && 0 >= Q && J >= K] f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && Q >= 2 && J >= K] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [H + -1*I >= 0 && K >= 1 + J] f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] f38(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f53(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f38(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f53(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True Signature: {(exitus616,7);(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Rule 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->{27,32},10->{14,15,16},11->{11,13},12->{12,24,29},13->{12,17},14->{10,17},15->{10,17},16->{10 ,17},17->{8,18},18->{5,6,7,19,20,21},19->{26,31},20->{28,33,34},21->{25,30},22->{1,23},23->{20}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] | +- p:[5,18,6,7,17,8,13,11,14,10,15,16] c: [5,6,7,8,10,11,13,14,15,16,17,18] | +- p:[12] c: [12] | `- p:[1,22,2] c: [1,2,22] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f2(A,H,I,J,K,P,Q) -> f13(1,H,I,J,K,P,Q) [A = 1] f13(A,H,I,J,K,P,Q) -> f16(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] f16(A,H,I,J,K,P,Q) -> f16(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [0 >= A] f2(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [A >= 2] f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [0 >= I && H >= I] f27(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,Q) [I >= 2 && H >= I] f27(A,H,I,J,K,P,Q) -> f35(A,H,1,J,K,P,Q) [H >= 1 && I = 1] f35(A,H,I,J,K,P,Q) -> f38(A,H,I,J,K,P,Q) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && 0 >= Q && J >= K] f38(A,H,I,J,K,P,Q) -> f53(A,H,I,J,K,P,Q) [H + -1*I >= 0 && Q >= 2 && J >= K] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && J >= K + 4*X && K + 5*X >= 1 + J && 0 >= K && J >= K && Q = 1] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,1) [H + -1*I >= 0 && J >= K + 4*X && K + 5*X >= 1 + J && J >= K && K >= 2 && Q = 1] f38(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,1) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && 0 >= K] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,1 + K,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && K >= 2] f53(A,H,I,J,K,P,Q) -> f38(A,H,I,J,2,P,Q) [H + -1*I >= 0 && J + -1*K >= 0 && Q >= 2*F1 && 3*F1 >= 1 + Q && K = 1] f38(A,H,I,J,K,P,Q) -> f35(A,H,I,J,K,P,1 + Q) [H + -1*I >= 0 && K >= 1 + J] f35(A,H,I,J,K,P,Q) -> f27(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [0 >= 2 + A && I >= 1 + H] f27(A,H,I,J,K,P,Q) -> f1(A,H,I,J,K,P,Q) [A >= 0 && I >= 1 + H] f27(A,H,I,J,K,P,Q) -> f1(-1,H,I,J,K,P,Q) [I >= 1 + H && 1 + A = 0] f16(A,H,I,J,K,P,Q) -> f13(A,H,1 + I,J,K,P,Q) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] f13(A,H,I,J,K,P,Q) -> f27(A,H,I,J,K,P,Q) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] f38(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f53(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f38(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f53(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True f1(A,H,I,J,K,P,Q) -> exitus616(A,H,I,J,K,P,Q) True Signature: {(exitus616,7);(f1,23);(f13,23);(f16,23);(f2,23);(f27,23);(f35,23);(f38,23);(f53,23)} Rule 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->{27,32},10->{14,15,16},11->{11,13},12->{12,24,29},13->{12,17},14->{10,17},15->{10,17},16->{10 ,17},17->{8,18},18->{5,6,7,19,20,21},19->{26,31},20->{28,33,34},21->{25,30},22->{1,23},23->{20}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] | +- p:[5,18,6,7,17,8,13,11,14,10,15,16] c: [5,6,7,8,10,11,13,14,15,16,17,18] | +- p:[12] c: [12] | `- p:[1,22,2] c: [1,2,22]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,H,I,J,K,P,Q,0.0,0.1,0.2] f2 ~> f13 [A <= K, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f13 ~> f16 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f16 ~> f16 [A <= A, H <= H, I <= I, J <= J, K <= K + K, P <= P, Q <= Q] f2 ~> f27 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f2 ~> f27 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f35 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f35 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f35 [A <= A, H <= H, I <= K, J <= J, K <= K, P <= P, Q <= Q] f35 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f38 ~> f53 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f38 ~> f53 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f38 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= K + K, P <= P, Q <= K] f38 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= J, P <= P, Q <= K] f38 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= 2*K, P <= P, Q <= K] f53 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= K + K, P <= P, Q <= Q] f53 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= J + K, P <= P, Q <= Q] f53 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= 2*K, P <= P, Q <= Q] f38 ~> f35 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= K + Q] f35 ~> f27 [A <= A, H <= H, I <= K + I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f1 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f1 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f1 [A <= K, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f16 ~> f13 [A <= A, H <= H, I <= K + I, J <= J, K <= K, P <= P, Q <= Q] f13 ~> f27 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f38 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f53 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f38 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f53 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f1 ~> exitus616 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] + Loop: [0.0 <= K + H + I + J + K + P + Q] f27 ~> f35 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f35 ~> f27 [A <= A, H <= H, I <= K + I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f35 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f27 ~> f35 [A <= A, H <= H, I <= K, J <= J, K <= K, P <= P, Q <= Q] f38 ~> f35 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= K + Q] f35 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f38 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= 2*K, P <= P, Q <= K] f38 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= K + K, P <= P, Q <= K] f53 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= K + K, P <= P, Q <= Q] f38 ~> f53 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f53 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= J + K, P <= P, Q <= Q] f53 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= 2*K, P <= P, Q <= Q] + Loop: [0.1 <= J + K] f38 ~> f38 [A <= A, H <= H, I <= I, J <= J, K <= J, P <= P, Q <= K] + Loop: [0.2 <= H + I + J + K] f13 ~> f16 [A <= A, H <= H, I <= I, J <= J, K <= K, P <= P, Q <= Q] f16 ~> f13 [A <= A, H <= H, I <= K + I, J <= J, K <= K, P <= P, Q <= Q] f16 ~> f16 [A <= A, H <= H, I <= I, J <= J, K <= K + K, P <= P, Q <= Q] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,H,I,J,K,P,Q,0.0,0.1,0.2] f2 ~> f13 [K ~=> A] f13 ~> f16 [] f16 ~> f16 [K ~+> K,K ~+> K] f2 ~> f27 [] f2 ~> f27 [] f27 ~> f35 [] f27 ~> f35 [] f27 ~> f35 [K ~=> I] f35 ~> f38 [] f38 ~> f53 [] f38 ~> f53 [] f38 ~> f38 [K ~=> Q,K ~+> K,K ~+> K] f38 ~> f38 [J ~=> K,K ~=> Q] f38 ~> f38 [K ~=> K,K ~=> Q] f53 ~> f38 [K ~+> K,K ~+> K] f53 ~> f38 [J ~+> K,K ~+> K] f53 ~> f38 [K ~=> K] f38 ~> f35 [Q ~+> Q,K ~+> Q] f35 ~> f27 [I ~+> I,K ~+> I] f27 ~> f1 [] f27 ~> f1 [] f27 ~> f1 [K ~=> A] f16 ~> f13 [I ~+> I,K ~+> I] f13 ~> f27 [] f38 ~> exitus616 [] f1 ~> exitus616 [] f1 ~> exitus616 [] f53 ~> exitus616 [] f1 ~> exitus616 [] f38 ~> exitus616 [] f1 ~> exitus616 [] f1 ~> exitus616 [] f53 ~> exitus616 [] f1 ~> exitus616 [] f1 ~> exitus616 [] + Loop: [H ~+> 0.0,I ~+> 0.0,J ~+> 0.0,K ~+> 0.0,P ~+> 0.0,Q ~+> 0.0,K ~+> 0.0] f27 ~> f35 [] f35 ~> f27 [I ~+> I,K ~+> I] f27 ~> f35 [] f27 ~> f35 [K ~=> I] f38 ~> f35 [Q ~+> Q,K ~+> Q] f35 ~> f38 [] f38 ~> f38 [K ~=> K,K ~=> Q] f38 ~> f38 [K ~=> Q,K ~+> K,K ~+> K] f53 ~> f38 [K ~+> K,K ~+> K] f38 ~> f53 [] f53 ~> f38 [J ~+> K,K ~+> K] f53 ~> f38 [K ~=> K] + Loop: [J ~+> 0.1,K ~+> 0.1] f38 ~> f38 [J ~=> K,K ~=> Q] + Loop: [H ~+> 0.2,I ~+> 0.2,J ~+> 0.2,K ~+> 0.2] f13 ~> f16 [] f16 ~> f13 [I ~+> I,K ~+> I] f16 ~> f16 [K ~+> K,K ~+> K] + Applied Processor: Lare + Details: f2 ~> exitus616 [J ~=> K ,K ~=> A ,K ~=> I ,K ~=> K ,K ~=> Q ,H ~+> 0.0 ,H ~+> 0.2 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> 0.2 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> 0.1 ,J ~+> 0.2 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,H ~*> 0.0 ,H ~*> 0.1 ,H ~*> tick ,I ~*> I ,I ~*> K ,I ~*> Q ,I ~*> 0.0 ,I ~*> 0.1 ,I ~*> tick ,J ~*> I ,J ~*> K ,J ~*> Q ,J ~*> 0.0 ,J ~*> 0.1 ,J ~*> tick ,K ~*> I ,K ~*> K ,K ~*> Q ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick ,P ~*> I ,P ~*> K ,P ~*> Q ,P ~*> 0.0 ,P ~*> 0.1 ,P ~*> tick ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,Q ~*> 0.0 ,Q ~*> 0.1 ,Q ~*> tick ,K ~*> I ,K ~*> K ,K ~*> Q ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] + f27> [K ~=> K ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,I ~*> I ,I ~*> K ,I ~*> Q ,J ~*> I ,J ~*> K ,J ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q ,P ~*> I ,P ~*> K ,P ~*> Q ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q] f53> [K ~=> I ,K ~=> K ,K ~=> Q ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,I ~*> I ,I ~*> K ,I ~*> Q ,J ~*> I ,J ~*> K ,J ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q ,P ~*> I ,P ~*> K ,P ~*> Q ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q] f38> [K ~=> I ,K ~=> K ,K ~=> Q ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,I ~*> I ,I ~*> K ,I ~*> Q ,J ~*> I ,J ~*> K ,J ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q ,P ~*> I ,P ~*> K ,P ~*> Q ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q] f27> [K ~=> K ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,I ~*> I ,I ~*> K ,I ~*> Q ,J ~*> I ,J ~*> K ,J ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q ,P ~*> I ,P ~*> K ,P ~*> Q ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q] f53> [K ~=> I ,K ~=> K ,K ~=> Q ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,I ~*> I ,I ~*> K ,I ~*> Q ,J ~*> I ,J ~*> K ,J ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q ,P ~*> I ,P ~*> K ,P ~*> Q ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q] f38> [K ~=> I ,K ~=> K ,K ~=> Q ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> 0.0 ,I ~+> tick ,J ~+> K ,J ~+> 0.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.0 ,K ~+> tick ,P ~+> 0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> Q ,K ~+> 0.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> Q ,I ~*> I ,I ~*> K ,I ~*> Q ,J ~*> I ,J ~*> K ,J ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q ,P ~*> I ,P ~*> K ,P ~*> Q ,Q ~*> I ,Q ~*> K ,Q ~*> Q ,K ~*> I ,K ~*> K ,K ~*> Q] + f38> [J ~=> K,K ~=> Q,J ~+> 0.1,J ~+> tick,K ~+> 0.1,K ~+> tick,tick ~+> tick] + f13> [H ~+> 0.2 ,H ~+> tick ,I ~+> I ,I ~+> 0.2 ,I ~+> tick ,J ~+> 0.2 ,J ~+> tick ,K ~+> K ,K ~+> 0.2 ,K ~+> tick ,tick ~+> tick ,K ~+> I ,K ~+> K ,H ~*> I ,H ~*> K ,I ~*> I ,I ~*> K ,J ~*> I ,J ~*> K ,K ~*> I ,K ~*> K ,K ~*> I ,K ~*> K] YES(?,POLY)