YES(?,POLY) * Step 1: ArgumentFilter WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(C2,I2,H2,M2,F2,F,G,H,I,J2,K,L,M,1,J,O2,N2,P2,S,T,U,V,W,X,Y,Z,A1,B1,Q2,D1,E1,G2,G1,H1,I1,J1,K1,L1,M1 [N = 1] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,N1,O1,P1,Q1,R1,D2,K2,E2,V1,W1,X1,Y1,Z1,A2,B2) 1. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(N,2,D2,H2,D2,F,G,H,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [N >= 2] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,P1,Q1,R1,C2,T1,D2,I2,W1,X1,Y1,Z1,A2,B2) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(C2,I2,H2,N2,M2,F,G,H,I,K2,K,L,M,J2,O,P2,O2,Q2,S,T,U,V,W,X,Y,Z,A1,B1,R2,D1,E1,E2,G1,H1,I1,J1,K1,L1,M1 [0 >= L2 && 0 >= N && 0 >= J2] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,N1,O1,P1,Q1,R1,D2,G2,F2,V1,W1,X1,Y1,Z1,A2,B2) 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(C2,I2,H2,N2,M2,F,G,H,I,K2,K,L,M,J2,O,P2,O2,Q2,S,T,U,V,W,X,Y,Z,A1,B1,R2,D1,E1,E2,G1,H1,I1,J1,K1,L1,M1 [-1*B + N >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,N1,O1,P1,Q1,R1,D2,G2,F2,V1,W1,X1,Y1,Z1,A2,B2) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(C2,I2,H2,M2,F2,F,G,H,I,J,J,E1,0,J2,O,O,N2,J,N2,T,U,V,W,X,Y,Z,A1,B1,J,D1,E1,G2,G1,H1,I1,J1,K1,L1,M1,N1[-1*B + N >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,R1,D2,K2,E2,V1,1 + E1,V,I,O2,P2,B2) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(C2,I2,H2,M2,F2,F,G,H,I,J,J,E1,0,J2,O,O,N2,J,N2,T,U,V,W,X,Y,Z,A1,B1,J,D1,E1,G2,G1,H1,I1,J1,K1,L1,M1,N1[-1*B + N >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,R1,D2,K2,E2,V1,1 + E1,V,I,O2,P2,B2) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,D,C2,D,D2,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [-1*B + N >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f7(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,C2,P,P,D2,J,D2,T,U,V,W,X,Y,Z,A1,B1,J,D1,-1 + E1,F1,G1,H1,I1,J1,H2,I2,V [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,I,K,1 + M,-1 + E1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,H2,K,L,M,C2,D2,K2,J2,G2,S,T,U,V,W,X,Y,Z,A1,B1,E2,D1,E1,I2,G1,H1,I1,J1,K1,L1,M1,N1 [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,F2,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,H2,K,L,M,C2,D2,K2,J2,G2,S,T,U,V,W,X,Y,Z,A1,B1,E2,D1,E1,I2,G1,H1,I1,J1,K1,L1,M1,N1 [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,F2,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,H2,K,L,M,C2,D2,K2,J2,G2,S,T,U,V,W,X,Y,Z,A1,B1,E2,D1,E1,I2,G1,H1,I1,J1,K1,L1,M1,N1 [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,F2,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,H2,K,L,M,C2,D2,K2,J2,G2,S,T,U,V,W,X,Y,Z,A1,B1,E2,D1,E1,I2,G1,H1,I1,J1,K1,L1,M1,N1 [-1*I + Y1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) ,O1,P1,Q1,F2,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] Signature: {(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6},2->{},3->{},4->{7,8,9,10,11,12,13,14,15,16,17,18},5->{7,8,9,10,11,12,13,14,15,16,17 ,18},6->{3,4,5,6},7->{7,8,9,10,11,12,13,14,15,16,17,18},8->{7,8,9,10,11,12,13,14,15,16,17,18},9->{7,8,9,10 ,11,12,13,14,15,16,17,18},10->{7,8,9,10,11,12,13,14,15,16,17,18},11->{7,8,9,10,11,12,13,14,15,16,17,18} ,12->{7,8,9,10,11,12,13,14,15,16,17,18},13->{7,8,9,10,11,12,13,14,15,16,17,18},14->{7,8,9,10,11,12,13,14,15 ,16,17,18},15->{},16->{},17->{},18->{}] + Applied Processor: ArgumentFilter [2,3,4,5,6,7,16,18,19,20,22,23,24,25,26,27,29,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,51,52,53] + Details: We remove following argument positions: [2 ,3 ,4 ,5 ,6 ,7 ,16 ,18 ,19 ,20 ,22 ,23 ,24 ,25 ,26 ,27 ,29 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,38 ,39 ,40 ,41 ,42 ,43 ,44 ,45 ,46 ,47 ,51 ,52 ,53]. * Step 2: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,J2,K,L,M,1,J,O2,P2,V,Q2,E1,W1,X1,Y1) [N = 1] (1,1) 1. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(N,2,I,J,K,L,M,N,C2,P,R,V,C1,E1,W1,X1,Y1) [N >= 2] (1,1) 2. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [0 >= L2 && 0 >= N && 0 >= J2] (1,1) 3. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(A,1 + B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] Signature: {(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6},2->{},3->{},4->{7,8,9,10,11,12,13,14,15,16,17,18},5->{7,8,9,10,11,12,13,14,15,16,17 ,18},6->{3,4,5,6},7->{7,8,9,10,11,12,13,14,15,16,17,18},8->{7,8,9,10,11,12,13,14,15,16,17,18},9->{7,8,9,10 ,11,12,13,14,15,16,17,18},10->{7,8,9,10,11,12,13,14,15,16,17,18},11->{7,8,9,10,11,12,13,14,15,16,17,18} ,12->{7,8,9,10,11,12,13,14,15,16,17,18},13->{7,8,9,10,11,12,13,14,15,16,17,18},14->{7,8,9,10,11,12,13,14,15 ,16,17,18},15->{},16->{},17->{},18->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,J2,K,L,M,1,J,O2,P2,V,Q2,E1,W1,X1,Y1) [N = 1] (1,1) 1. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(N,2,I,J,K,L,M,N,C2,P,R,V,C1,E1,W1,X1,Y1) [N >= 2] (1,1) 2. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [0 >= L2 && 0 >= N && 0 >= J2] (1,1) 3. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [-1*B + N >= 0 (1,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (1,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (1,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(A,1 + B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] Signature: {(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6},2->{},3->{},4->{7,8,9,10,11,12,13,14,15,16,17,18},5->{7,8,9,10,11,12,13,14,15,16,17 ,18},6->{3,4,5,6},7->{7,8,9,10,11,12,13,14,15,16,17,18},8->{7,8,9,10,11,12,13,14,15,16,17,18},9->{7,8,9,10 ,11,12,13,14,15,16,17,18},10->{7,8,9,10,11,12,13,14,15,16,17,18},11->{7,8,9,10,11,12,13,14,15,16,17,18} ,12->{7,8,9,10,11,12,13,14,15,16,17,18},13->{7,8,9,10,11,12,13,14,15,16,17,18},14->{7,8,9,10,11,12,13,14,15 ,16,17,18},15->{},16->{},17->{},18->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,15) ,(4,16) ,(4,17) ,(4,18) ,(5,15) ,(5,16) ,(5,17) ,(5,18)] * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,J2,K,L,M,1,J,O2,P2,V,Q2,E1,W1,X1,Y1) [N = 1] (1,1) 1. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(N,2,I,J,K,L,M,N,C2,P,R,V,C1,E1,W1,X1,Y1) [N >= 2] (1,1) 2. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [0 >= L2 && 0 >= N && 0 >= J2] (1,1) 3. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [-1*B + N >= 0 (1,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (1,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (1,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(A,1 + B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (1,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] Signature: {(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6},2->{},3->{},4->{7,8,9,10,11,12,13,14},5->{7,8,9,10,11,12,13,14},6->{3,4,5,6},7->{7,8,9 ,10,11,12,13,14,15,16,17,18},8->{7,8,9,10,11,12,13,14,15,16,17,18},9->{7,8,9,10,11,12,13,14,15,16,17,18} ,10->{7,8,9,10,11,12,13,14,15,16,17,18},11->{7,8,9,10,11,12,13,14,15,16,17,18},12->{7,8,9,10,11,12,13,14,15 ,16,17,18},13->{7,8,9,10,11,12,13,14,15,16,17,18},14->{7,8,9,10,11,12,13,14,15,16,17,18},15->{},16->{} ,17->{},18->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,J2,K,L,M,1,J,O2,P2,V,Q2,E1,W1,X1,Y1) [N = 1] (1,1) 1. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(N,2,I,J,K,L,M,N,C2,P,R,V,C1,E1,W1,X1,Y1) [N >= 2] (1,1) 2. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [0 >= L2 && 0 >= N && 0 >= J2] (1,1) 3. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(A,1 + B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] 19. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (1,1) 20. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (?,1) 21. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (?,1) Signature: {(exitus616,17);(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6,21},2->{},3->{},4->{7,8,9,10,11,12,13,14,15,16,17,18,20},5->{7,8,9,10,11,12,13,14,15,16 ,17,18,20},6->{3,4,5,6,21},7->{7,8,9,10,11,12,13,14,15,16,17,18,20},8->{7,8,9,10,11,12,13,14,15,16,17,18,20} ,9->{7,8,9,10,11,12,13,14,15,16,17,18,20},10->{7,8,9,10,11,12,13,14,15,16,17,18,20},11->{7,8,9,10,11,12,13 ,14,15,16,17,18,20},12->{7,8,9,10,11,12,13,14,15,16,17,18,20},13->{7,8,9,10,11,12,13,14,15,16,17,18,20} ,14->{7,8,9,10,11,12,13,14,15,16,17,18,20},15->{},16->{},17->{},18->{},19->{},20->{},21->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,15) ,(4,16) ,(4,17) ,(4,18) ,(5,15) ,(5,16) ,(5,17) ,(5,18)] * Step 6: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,J2,K,L,M,1,J,O2,P2,V,Q2,E1,W1,X1,Y1) [N = 1] (1,1) 1. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(N,2,I,J,K,L,M,N,C2,P,R,V,C1,E1,W1,X1,Y1) [N >= 2] (1,1) 2. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [0 >= L2 && 0 >= N && 0 >= J2] (1,1) 3. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(A,1 + B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] 19. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (1,1) 20. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (?,1) 21. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (?,1) Signature: {(exitus616,17);(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6,21},2->{},3->{},4->{7,8,9,10,11,12,13,14,20},5->{7,8,9,10,11,12,13,14,20},6->{3,4,5,6 ,21},7->{7,8,9,10,11,12,13,14,15,16,17,18,20},8->{7,8,9,10,11,12,13,14,15,16,17,18,20},9->{7,8,9,10,11,12,13 ,14,15,16,17,18,20},10->{7,8,9,10,11,12,13,14,15,16,17,18,20},11->{7,8,9,10,11,12,13,14,15,16,17,18,20} ,12->{7,8,9,10,11,12,13,14,15,16,17,18,20},13->{7,8,9,10,11,12,13,14,15,16,17,18,20},14->{7,8,9,10,11,12,13 ,14,15,16,17,18,20},15->{},16->{},17->{},18->{},19->{},20->{},21->{}] + Applied Processor: LooptreeTransformer + 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] | +- p:[6] c: [6] | `- p:[7,8,9,10,11,12,13,14] c: [14] | `- p:[7,8,9,10,11,12,13] c: [13] | `- p:[7,8,9,10,11,12] c: [12] | `- p:[7,8,9,10,11] c: [11] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7] * Step 7: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,J2,K,L,M,1,J,O2,P2,V,Q2,E1,W1,X1,Y1) [N = 1] (1,1) 1. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(N,2,I,J,K,L,M,N,C2,P,R,V,C1,E1,W1,X1,Y1) [N >= 2] (1,1) 2. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [0 >= L2 && 0 >= N && 0 >= J2] (1,1) 3. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(C2,I2,I,K2,K,L,M,J2,O,P2,Q2,V,R2,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && L2 >= 2 && W1 >= L2 && J2 >= 2 && W1 >= J2 && B >= A && W1 >= 0 && B >= 0 && O = J] 4. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && K >= 1 + O && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 5. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(C2,I2,I,J,J,E1,0,J2,O,O,J,V,J,E1,1 + E1,V,I) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && Q2 >= 2 && W1 >= Q2 && J2 >= 2 && W1 >= J2 && O >= 1 + K && B >= A && B >= 0 && W1 >= 0 && M = 0 && J = K] 6. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f1(A,1 + B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) [-1*B + N >= 0 (?,1) && A + -1*B >= 0 && -2 + B >= 0 && -4 + B + N >= 0 && -4 + A + B >= 0 && A + -1*N >= 0 && -2 + N >= 0 && -4 + A + N >= 0 && -1*A + N >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] 7. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 8. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 9. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 10. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && K2 >= 1 + J2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 11. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && I2 >= 1 + J2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 12. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J >= 1 + J2 && J2 >= 1 + I2 && K >= 1 + J2 && G2 >= 0 && C2 >= 2 && E1 >= 0] 13. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && I2 >= 1 + J2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 14. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f7(A,B,I,J,K,L,1 + M,C2,P,P,J,V,J,-1 + E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && J2 >= 1 + K2 && J2 >= 1 + J && J2 >= 1 + I2 && J2 >= 1 + K && G2 >= 0 && C2 >= 2 && E1 >= 0] 15. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && K >= 1 + D2 && J = P] 16. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && F2 >= 1 + D2 && D2 >= 1 + K && J = P] 17. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && K >= 1 + D2 && J = P] 18. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> f4(A,B,I,H2,K,L,M,C2,D2,K2,G2,V,E2,E1,W1,X1,Y1) [-1*I + Y1 >= 0 (?,1) && I + -1*Y1 >= 0 && V + -1*X1 >= 0 && -1*V + X1 >= 0 && 1 + L + -1*W1 >= 0 && -1 + -1*E1 + W1 >= 0 && -1 + -1*L + W1 >= 0 && -1*E1 + L >= 0 && -1*C1 + R >= 0 && -1*C1 + K >= 0 && -1*C1 + J >= 0 && C1 + -1*R >= 0 && C1 + -1*K >= 0 && C1 + -1*J >= 0 && K + -1*R >= 0 && J + -1*R >= 0 && -1*K + R >= 0 && -1*J + R >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && -2 + N >= 0 && -2 + M + N >= 0 && M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E1 >= 0 && C2 >= 2 && D2 >= 1 + F2 && D2 >= 1 + K && J = P] 19. f3(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (1,1) 20. f7(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (?,1) 21. f1(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) -> exitus616(A,B,I,J,K,L,M,N,O,P,R,V,C1,E1,W1,X1,Y1) True (?,1) Signature: {(exitus616,17);(f1,54);(f3,54);(f4,54);(f7,54)} Flow Graph: [0->{},1->{3,4,5,6,21},2->{},3->{},4->{7,8,9,10,11,12,13,14,20},5->{7,8,9,10,11,12,13,14,20},6->{3,4,5,6 ,21},7->{7,8,9,10,11,12,13,14,15,16,17,18,20},8->{7,8,9,10,11,12,13,14,15,16,17,18,20},9->{7,8,9,10,11,12,13 ,14,15,16,17,18,20},10->{7,8,9,10,11,12,13,14,15,16,17,18,20},11->{7,8,9,10,11,12,13,14,15,16,17,18,20} ,12->{7,8,9,10,11,12,13,14,15,16,17,18,20},13->{7,8,9,10,11,12,13,14,15,16,17,18,20},14->{7,8,9,10,11,12,13 ,14,15,16,17,18,20},15->{},16->{},17->{},18->{},19->{},20->{},21->{}] ,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] | +- p:[6] c: [6] | `- p:[7,8,9,10,11,12,13,14] c: [14] | `- p:[7,8,9,10,11,12,13] c: [13] | `- p:[7,8,9,10,11,12] c: [12] | `- p:[7,8,9,10,11] c: [11] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 8: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A ,B ,I ,J ,K ,L ,M ,N ,O ,P ,R ,V ,C1 ,E1 ,W1 ,X1 ,Y1 ,0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.0.0.0 ,0.1.0.0.0.0.0 ,0.1.0.0.0.0.0.0 ,0.1.0.0.0.0.0.0.0] f3 ~> f4 [A <= unknown, B <= unknown, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= K, O <= J, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f3 ~> f1 [A <= N, B <= 2*K, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= unknown, P <= P, R <= R, V <= V, C1 <= C1, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f3 ~> f4 [A <= unknown, B <= unknown, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= unknown, O <= O, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f1 ~> f4 [A <= unknown, B <= unknown, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= W1, O <= O, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f1 ~> f7 [A <= unknown, B <= unknown, I <= I, J <= J, K <= J, L <= E1, M <= 0*K, N <= W1, O <= O, P <= O, R <= J, V <= V, C1 <= J, E1 <= E1, W1 <= K + E1, X1 <= V, Y1 <= I] f1 ~> f7 [A <= unknown, B <= unknown, I <= I, J <= J, K <= J, L <= E1, M <= 0*K, N <= W1, O <= O, P <= O, R <= J, V <= V, C1 <= J, E1 <= E1, W1 <= K + E1, X1 <= V, Y1 <= I] f1 ~> f1 [A <= A, B <= N, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, R <= R, V <= V, C1 <= C1, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f4 [A <= A, B <= B, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f4 [A <= A, B <= B, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f4 [A <= A, B <= B, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f4 [A <= A, B <= B, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= unknown, R <= unknown, V <= V, C1 <= unknown, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f3 ~> exitus616 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, R <= R, V <= V, C1 <= C1, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> exitus616 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, R <= R, V <= V, C1 <= C1, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] f1 ~> exitus616 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, R <= R, V <= V, C1 <= C1, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.0 <= K + A + B] f1 ~> f1 [A <= A, B <= N, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, R <= R, V <= V, C1 <= C1, E1 <= E1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1 <= E1 + W1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0 <= E1 + W1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0.0 <= E1 + W1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0.0.0 <= E1 + W1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0.0.0.0 <= E1 + L + W1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0.0.0.0.0 <= K + E1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0.0.0.0.0.0 <= K + E1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Loop: [0.1.0.0.0.0.0.0.0 <= K + E1] f7 ~> f7 [A <= A, B <= B, I <= I, J <= J, K <= K, L <= L, M <= M + N, N <= unknown, O <= P, P <= P, R <= J, V <= V, C1 <= J, E1 <= W1, W1 <= W1, X1 <= X1, Y1 <= Y1] + Applied Processor: FlowAbstraction + Details: () * Step 9: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick ,huge ,K ,A ,B ,I ,J ,K ,L ,M ,N ,O ,P ,R ,V ,C1 ,E1 ,W1 ,X1 ,Y1 ,0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.0.0.0 ,0.1.0.0.0.0.0 ,0.1.0.0.0.0.0.0 ,0.1.0.0.0.0.0.0.0] f3 ~> f4 [J ~=> O,K ~=> N,huge ~=> A,huge ~=> B,huge ~=> C1,huge ~=> J,huge ~=> P,huge ~=> R] f3 ~> f1 [N ~=> A,K ~=> B,huge ~=> O] f3 ~> f4 [huge ~=> A,huge ~=> B,huge ~=> C1,huge ~=> J,huge ~=> N,huge ~=> P,huge ~=> R] f1 ~> f4 [W1 ~=> N,huge ~=> A,huge ~=> B,huge ~=> C1,huge ~=> J,huge ~=> P,huge ~=> R] f1 ~> f7 [E1 ~=> L ,I ~=> Y1 ,J ~=> C1 ,J ~=> K ,J ~=> R ,O ~=> P ,V ~=> X1 ,W1 ~=> N ,K ~=> M ,huge ~=> A ,huge ~=> B ,E1 ~+> W1 ,K ~+> W1] f1 ~> f7 [E1 ~=> L ,I ~=> Y1 ,J ~=> C1 ,J ~=> K ,J ~=> R ,O ~=> P ,V ~=> X1 ,W1 ~=> N ,K ~=> M ,huge ~=> A ,huge ~=> B ,E1 ~+> W1 ,K ~+> W1] f1 ~> f1 [N ~=> B] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f4 [huge ~=> C1,huge ~=> J,huge ~=> N,huge ~=> O,huge ~=> P,huge ~=> R] f7 ~> f4 [huge ~=> C1,huge ~=> J,huge ~=> N,huge ~=> O,huge ~=> P,huge ~=> R] f7 ~> f4 [huge ~=> C1,huge ~=> J,huge ~=> N,huge ~=> O,huge ~=> P,huge ~=> R] f7 ~> f4 [huge ~=> C1,huge ~=> J,huge ~=> N,huge ~=> O,huge ~=> P,huge ~=> R] f3 ~> exitus616 [] f7 ~> exitus616 [] f1 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f1 ~> f1 [N ~=> B] + Loop: [E1 ~+> 0.1,W1 ~+> 0.1] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0,W1 ~+> 0.1.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0.0,W1 ~+> 0.1.0.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0.0.0,W1 ~+> 0.1.0.0.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0.0.0.0,L ~+> 0.1.0.0.0.0,W1 ~+> 0.1.0.0.0.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0.0.0.0.0,K ~+> 0.1.0.0.0.0.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0.0.0.0.0.0,K ~+> 0.1.0.0.0.0.0.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Loop: [E1 ~+> 0.1.0.0.0.0.0.0.0,K ~+> 0.1.0.0.0.0.0.0.0] f7 ~> f7 [J ~=> C1,J ~=> R,P ~=> O,W1 ~=> E1,huge ~=> N,M ~+> M,N ~+> M] + Applied Processor: LareProcessor + Details: f3 ~> f4 [E1 ~=> L ,I ~=> Y1 ,J ~=> K ,J ~=> O ,V ~=> X1 ,W1 ~=> N ,K ~=> M ,K ~=> N ,huge ~=> A ,huge ~=> B ,huge ~=> C1 ,huge ~=> J ,huge ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> R ,E1 ~+> E1 ,E1 ~+> W1 ,E1 ~+> 0.1 ,E1 ~+> 0.1.0 ,E1 ~+> 0.1.0.0 ,E1 ~+> 0.1.0.0.0 ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,N ~+> 0.0 ,N ~+> tick ,W1 ~+> M ,tick ~+> tick ,K ~+> E1 ,K ~+> M ,K ~+> W1 ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> 0.1 ,E1 ~*> 0.1.0 ,E1 ~*> 0.1.0.0 ,E1 ~*> 0.1.0.0.0 ,E1 ~*> 0.1.0.0.0.0 ,E1 ~*> tick ,K ~*> M ,K ~*> 0.0 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0.0.0 ,K ~*> tick ,huge ~*> M] f3 ~> exitus616 [E1 ~=> L ,I ~=> Y1 ,J ~=> C1 ,J ~=> K ,J ~=> R ,N ~=> A ,N ~=> B ,V ~=> X1 ,W1 ~=> N ,K ~=> B ,K ~=> M ,huge ~=> A ,huge ~=> B ,huge ~=> N ,huge ~=> O ,huge ~=> P ,E1 ~+> E1 ,E1 ~+> W1 ,E1 ~+> 0.1 ,E1 ~+> 0.1.0 ,E1 ~+> 0.1.0.0 ,E1 ~+> 0.1.0.0.0 ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,N ~+> 0.0 ,N ~+> tick ,W1 ~+> M ,tick ~+> tick ,K ~+> E1 ,K ~+> M ,K ~+> W1 ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> 0.1 ,E1 ~*> 0.1.0 ,E1 ~*> 0.1.0.0 ,E1 ~*> 0.1.0.0.0 ,E1 ~*> 0.1.0.0.0.0 ,E1 ~*> tick ,K ~*> M ,K ~*> 0.0 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0.0.0 ,K ~*> tick ,huge ~*> M] + f1> [N ~=> B,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick,K ~+> 0.0,K ~+> tick] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1 ,E1 ~+> 0.1.0 ,E1 ~+> 0.1.0.0 ,E1 ~+> 0.1.0.0.0 ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,L ~+> 0.1.0.0.0.0 ,L ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1 ,W1 ~+> 0.1.0 ,W1 ~+> 0.1.0.0 ,W1 ~+> 0.1.0.0.0 ,W1 ~+> 0.1.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,L ~*> M ,L ~*> tick ,W1 ~*> M ,W1 ~*> 0.1.0 ,W1 ~*> 0.1.0.0 ,W1 ~*> 0.1.0.0.0 ,W1 ~*> 0.1.0.0.0.0 ,W1 ~*> tick ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0 ,E1 ~+> 0.1.0.0 ,E1 ~+> 0.1.0.0.0 ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,L ~+> 0.1.0.0.0.0 ,L ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1.0 ,W1 ~+> 0.1.0.0 ,W1 ~+> 0.1.0.0.0 ,W1 ~+> 0.1.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,L ~*> M ,L ~*> tick ,W1 ~*> M ,W1 ~*> 0.1.0.0 ,W1 ~*> 0.1.0.0.0 ,W1 ~*> 0.1.0.0.0.0 ,W1 ~*> tick ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0.0 ,E1 ~+> 0.1.0.0.0 ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,L ~+> 0.1.0.0.0.0 ,L ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1.0.0 ,W1 ~+> 0.1.0.0.0 ,W1 ~+> 0.1.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,L ~*> M ,L ~*> tick ,W1 ~*> M ,W1 ~*> 0.1.0.0.0 ,W1 ~*> 0.1.0.0.0.0 ,W1 ~*> tick ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0.0.0 ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,L ~+> 0.1.0.0.0.0 ,L ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1.0.0.0 ,W1 ~+> 0.1.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,L ~*> M ,L ~*> tick ,W1 ~*> M ,W1 ~*> 0.1.0.0.0.0 ,W1 ~*> tick ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,L ~+> 0.1.0.0.0.0 ,L ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,L ~*> M ,L ~*> tick ,W1 ~*> M ,W1 ~*> tick ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1.0.0.0.0.0.0 ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,W1 ~*> M ,W1 ~*> tick ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0.0.0.0.0.0 ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,M ~+> M ,N ~+> M ,W1 ~+> 0.1.0.0.0.0.0.0.0 ,W1 ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0.0 ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,E1 ~*> tick ,W1 ~*> M ,K ~*> M ,K ~*> tick ,huge ~*> M] + f7> [J ~=> C1 ,J ~=> R ,P ~=> O ,W1 ~=> E1 ,huge ~=> N ,E1 ~+> 0.1.0.0.0.0.0.0.0 ,E1 ~+> tick ,M ~+> M ,N ~+> M ,tick ~+> tick ,K ~+> 0.1.0.0.0.0.0.0.0 ,K ~+> tick ,huge ~+> M ,E1 ~*> M ,K ~*> M] YES(?,POLY)