MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f17(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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 1. f17(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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 2. f17(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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 3. f9(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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [-2 + B >= 0 (?,1) ,M1,N1) && -4 + B + J >= 0 && -2 + J >= 0 && I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] 4. f9(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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [-2 + B >= 0 (?,1) ,C2,N1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 5. f9(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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [-2 + B >= 0 (?,1) ,C2,N1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 6. f9(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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [-2 + B >= 0 (?,1) ,C2,N1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 7. f9(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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [-2 + B >= 0 (?,1) ,C2,N1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 8. f9(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) -> f9(A,1 + B,D,O1,D,P1,B,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) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] (?,1) 9. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 10. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 11. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 12. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 13. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 14. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 15. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 16. f16(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) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [-1 + -1*I + L1 >= 0 (?,1) ,I1,J1,K1,L1,M1,N1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 17. f16(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) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [-1 + -1*I + L1 >= 0 (?,1) ,J1,K1,L1,M1,0) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] 18. f16(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) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [-1 + -1*I + L1 >= 0 (?,1) ,J1,K1,L1,M1,0) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] 19. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] 20. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] 21. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] 22. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] 23. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] 24. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] 25. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] 26. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [-1 + -1*I + L1 >= 0 (?,1) ,K1,L1,M1,N1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] 27. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] 28. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && V1 >= 1 && O1 >= 2 && Z = X] Signature: {(f16,40);(f17,40);(f18,40);(f7,40);(f9,40)} Flow Graph: [0->{},1->{},2->{3,4,5,6,7,8},3->{},4->{9,10,11,12,13,14,15,16,17,18},5->{9,10,11,12,13,14,15,16,17,18} ,6->{9,10,11,12,13,14,15,16,17,18},7->{9,10,11,12,13,14,15,16,17,18},8->{3,4,5,6,7,8},9->{9,10,11,12,13,14 ,15,16,17,18},10->{9,10,11,12,13,14,15,16,17,18},11->{9,10,11,12,13,14,15,16,17,18},12->{9,10,11,12,13,14,15 ,16,17,18},13->{9,10,11,12,13,14,15,16,17,18},14->{9,10,11,12,13,14,15,16,17,18},15->{9,10,11,12,13,14,15,16 ,17,18},16->{9,10,11,12,13,14,15,16,17,18},17->{19,20,21,22,23,24,25,26,27,28},18->{19,20,21,22,23,24,25,26 ,27,28},19->{19,20,21,22,23,24,25,26,27,28},20->{19,20,21,22,23,24,25,26,27,28},21->{19,20,21,22,23,24,25,26 ,27,28},22->{19,20,21,22,23,24,25,26,27,28},23->{19,20,21,22,23,24,25,26,27,28},24->{19,20,21,22,23,24,25,26 ,27,28},25->{19,20,21,22,23,24,25,26,27,28},26->{19,20,21,22,23,24,25,26,27,28},27->{},28->{}] + Applied Processor: ArgumentFilter [3,4,5,6,13,14,15,18,19,20,21,22,24,26,28,30,31,32,33,34,35,36,38] + Details: We remove following argument positions: [3,4,5,6,13,14,15,18,19,20,21,22,24,26,28,30,31,32,33,34,35,36,38]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,1,D,B2,D,Q,R,G2,Y1,H2,D1,L1,N1) True (1,1) 1. f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(S1,T1,Q1,X1,I,P1,K,C2,K,Q,R,H2,G2,I2,D1,L1,N1) [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) 2. f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(P1,2,R1,H,I,P1,S1,L,M,Q,R,X,Z,B1,D1,L1,N1) [P1 >= 2] (1,1) 3. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,O1,C,B2,C,Q,R,G2,Y1,H2,D1,L1,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] 4. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 5. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 6. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 7. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 8. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(A,1 + B,D,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] (?,1) 9. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 10. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 11. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 12. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 13. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 14. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 15. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 16. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 17. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] 18. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] 19. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] 20. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] 21. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] 22. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] 23. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] 24. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] 25. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] 26. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] 27. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] 28. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && V1 >= 1 && O1 >= 2 && Z = X] Signature: {(f16,40);(f17,40);(f18,40);(f7,40);(f9,40)} Flow Graph: [0->{},1->{},2->{3,4,5,6,7,8},3->{},4->{9,10,11,12,13,14,15,16,17,18},5->{9,10,11,12,13,14,15,16,17,18} ,6->{9,10,11,12,13,14,15,16,17,18},7->{9,10,11,12,13,14,15,16,17,18},8->{3,4,5,6,7,8},9->{9,10,11,12,13,14 ,15,16,17,18},10->{9,10,11,12,13,14,15,16,17,18},11->{9,10,11,12,13,14,15,16,17,18},12->{9,10,11,12,13,14,15 ,16,17,18},13->{9,10,11,12,13,14,15,16,17,18},14->{9,10,11,12,13,14,15,16,17,18},15->{9,10,11,12,13,14,15,16 ,17,18},16->{9,10,11,12,13,14,15,16,17,18},17->{19,20,21,22,23,24,25,26,27,28},18->{19,20,21,22,23,24,25,26 ,27,28},19->{19,20,21,22,23,24,25,26,27,28},20->{19,20,21,22,23,24,25,26,27,28},21->{19,20,21,22,23,24,25,26 ,27,28},22->{19,20,21,22,23,24,25,26,27,28},23->{19,20,21,22,23,24,25,26,27,28},24->{19,20,21,22,23,24,25,26 ,27,28},25->{19,20,21,22,23,24,25,26,27,28},26->{19,20,21,22,23,24,25,26,27,28},27->{},28->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,17) ,(4,18) ,(5,17) ,(5,18) ,(6,17) ,(6,18) ,(7,17) ,(7,18) ,(17,26) ,(17,27) ,(17,28) ,(18,19) ,(18,27) ,(18,28) ,(19,26) ,(19,27) ,(19,28) ,(26,19) ,(26,27) ,(26,28)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,1,D,B2,D,Q,R,G2,Y1,H2,D1,L1,N1) True (1,1) 1. f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(S1,T1,Q1,X1,I,P1,K,C2,K,Q,R,H2,G2,I2,D1,L1,N1) [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) 2. f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(P1,2,R1,H,I,P1,S1,L,M,Q,R,X,Z,B1,D1,L1,N1) [P1 >= 2] (1,1) 3. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,O1,C,B2,C,Q,R,G2,Y1,H2,D1,L1,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] 4. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 5. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 6. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 7. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 (?,1) && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 8. f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(A,1 + B,D,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] (?,1) 9. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 10. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 11. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 12. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 13. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 14. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 15. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] 16. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] 17. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] 18. f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 (?,1) && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] 19. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] 20. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] 21. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] 22. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] 23. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] 24. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] 25. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] 26. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] 27. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] 28. f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 (?,1) && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && V1 >= 1 && O1 >= 2 && Z = X] Signature: {(f16,40);(f17,40);(f18,40);(f7,40);(f9,40)} Flow Graph: [0->{},1->{},2->{3,4,5,6,7,8},3->{},4->{9,10,11,12,13,14,15,16},5->{9,10,11,12,13,14,15,16},6->{9,10,11,12 ,13,14,15,16},7->{9,10,11,12,13,14,15,16},8->{3,4,5,6,7,8},9->{9,10,11,12,13,14,15,16,17,18},10->{9,10,11,12 ,13,14,15,16,17,18},11->{9,10,11,12,13,14,15,16,17,18},12->{9,10,11,12,13,14,15,16,17,18},13->{9,10,11,12,13 ,14,15,16,17,18},14->{9,10,11,12,13,14,15,16,17,18},15->{9,10,11,12,13,14,15,16,17,18},16->{9,10,11,12,13,14 ,15,16,17,18},17->{19,20,21,22,23,24,25},18->{20,21,22,23,24,25,26},19->{19,20,21,22,23,24,25},20->{19,20,21 ,22,23,24,25,26,27,28},21->{19,20,21,22,23,24,25,26,27,28},22->{19,20,21,22,23,24,25,26,27,28},23->{19,20,21 ,22,23,24,25,26,27,28},24->{19,20,21,22,23,24,25,26,27,28},25->{19,20,21,22,23,24,25,26,27,28},26->{20,21,22 ,23,24,25,26},27->{},28->{}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,1,D,B2,D,Q,R,G2,Y1,H2,D1,L1,N1) True f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(S1,T1,Q1,X1,I,P1,K,C2,K,Q,R,H2,G2,I2,D1,L1,N1) [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(P1,2,R1,H,I,P1,S1,L,M,Q,R,X,Z,B1,D1,L1,N1) [P1 >= 2] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,O1,C,B2,C,Q,R,G2,Y1,H2,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(A,1 + B,D,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && V1 >= 1 && O1 >= 2 && Z = X] Signature: {(f16,40);(f17,40);(f18,40);(f7,40);(f9,40)} Rule Graph: [0->{},1->{},2->{3,4,5,6,7,8},3->{},4->{9,10,11,12,13,14,15,16},5->{9,10,11,12,13,14,15,16},6->{9,10,11,12 ,13,14,15,16},7->{9,10,11,12,13,14,15,16},8->{3,4,5,6,7,8},9->{9,10,11,12,13,14,15,16,17,18},10->{9,10,11,12 ,13,14,15,16,17,18},11->{9,10,11,12,13,14,15,16,17,18},12->{9,10,11,12,13,14,15,16,17,18},13->{9,10,11,12,13 ,14,15,16,17,18},14->{9,10,11,12,13,14,15,16,17,18},15->{9,10,11,12,13,14,15,16,17,18},16->{9,10,11,12,13,14 ,15,16,17,18},17->{19,20,21,22,23,24,25},18->{20,21,22,23,24,25,26},19->{19,20,21,22,23,24,25},20->{19,20,21 ,22,23,24,25,26,27,28},21->{19,20,21,22,23,24,25,26,27,28},22->{19,20,21,22,23,24,25,26,27,28},23->{19,20,21 ,22,23,24,25,26,27,28},24->{19,20,21,22,23,24,25,26,27,28},25->{19,20,21,22,23,24,25,26,27,28},26->{20,21,22 ,23,24,25,26},27->{},28->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose MAYBE + Considered Problem: Rules: f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,1,D,B2,D,Q,R,G2,Y1,H2,D1,L1,N1) True f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(S1,T1,Q1,X1,I,P1,K,C2,K,Q,R,H2,G2,I2,D1,L1,N1) [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(P1,2,R1,H,I,P1,S1,L,M,Q,R,X,Z,B1,D1,L1,N1) [P1 >= 2] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,O1,C,B2,C,Q,R,G2,Y1,H2,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(A,1 + B,D,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && V1 >= 1 && O1 >= 2 && Z = X] f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True Signature: {(exitus616,17);(f16,40);(f17,40);(f18,40);(f7,40);(f9,40)} Rule Graph: [0->{47},1->{46},2->{3,4,5,6,7,8},3->{45},4->{9,10,11,12,13,14,15,16},5->{9,10,11,12,13,14,15,16},6->{9,10 ,11,12,13,14,15,16},7->{9,10,11,12,13,14,15,16},8->{3,4,5,6,7,8},9->{9,10,11,12,13,14,15,16,17,18},10->{9,10 ,11,12,13,14,15,16,17,18},11->{9,10,11,12,13,14,15,16,17,18},12->{9,10,11,12,13,14,15,16,17,18},13->{9,10,11 ,12,13,14,15,16,17,18},14->{9,10,11,12,13,14,15,16,17,18},15->{9,10,11,12,13,14,15,16,17,18},16->{9,10,11,12 ,13,14,15,16,17,18},17->{19,20,21,22,23,24,25},18->{20,21,22,23,24,25,26},19->{19,20,21,22,23,24,25},20->{19 ,20,21,22,23,24,25,26,27,28},21->{19,20,21,22,23,24,25,26,27,28},22->{19,20,21,22,23,24,25,26,27,28},23->{19 ,20,21,22,23,24,25,26,27,28},24->{19,20,21,22,23,24,25,26,27,28},25->{19,20,21,22,23,24,25,26,27,28},26->{20 ,21,22,23,24,25,26},27->{30,32,34,36,38,40,42,44},28->{29,31,33,35,37,39,41,43}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47] | +- p:[8] c: [8] | +- p:[9,10,11,12,13,14,15,16] c: [9,10,11,12,13,14,15,16] | `- p:[19,20,21,22,23,24,25,26] c: [19,20,21,22,23,24,25,26] * Step 6: AbstractSize MAYBE + Considered Problem: (Rules: f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,1,D,B2,D,Q,R,G2,Y1,H2,D1,L1,N1) True f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(S1,T1,Q1,X1,I,P1,K,C2,K,Q,R,H2,G2,I2,D1,L1,N1) [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] f17(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(P1,2,R1,H,I,P1,S1,L,M,Q,R,X,Z,B1,D1,L1,N1) [P1 >= 2] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(P1,Q1,R1,C2,I,O1,C,B2,C,Q,R,G2,Y1,H2,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(P1,Q1,R1,C,R,O1,K,K,Z1,1,R,X,Z,B1,D1,1 + R,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && X1 >= O1 && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] f9(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f9(A,1 + B,D,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f16(A,B,C,H,I,O1,L,L,P1,1 + Q,-1 + R,X,Z,B1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] f16(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,R1,I,O1,K,S1,M,1 + D1 + -1*R,R,M,K,M,D1,L1,0) [-1 + -1*I + L1 >= 0 && 1 + I + -1*L1 >= 0 && I + -1*R >= 0 && -1 + L1 + -1*R >= 0 && -2 + B >= 0 && -3 + B + Q >= 0 && -4 + B + J >= 0 && -1 + Q >= 0 && -3 + J + Q >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && -2 + J >= 0 && Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f7(A,B,C,H,I,O1,Z,L,P1,Q,0,X,Z,X,-1 + D1 + R,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] f7(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> f18(A,B,C,H,I,O1,K,L,M,Q,R,Q1,R1,T1,D1,L1,N1) [-1 + -1*I + L1 >= 0 && I >= 0 && I + N1 >= 0 && I + -1*N1 >= 0 && -1 + I + L1 >= 0 && 1 + I + -1*L1 >= 0 && -2 + B + I >= 0 && I + R >= 0 && I + -1*R >= 0 && -2 + I + J >= 0 && -1*N1 >= 0 && -1 + L1 + -1*N1 >= 0 && -2 + B + -1*N1 >= 0 && -1*N1 + R >= 0 && -2 + J + -1*N1 >= 0 && N1 >= 0 && -1 + L1 + N1 >= 0 && -2 + B + N1 >= 0 && N1 + R >= 0 && -2 + J + N1 >= 0 && -1 + L1 >= 0 && -3 + B + L1 >= 0 && -1 + L1 + R >= 0 && -1 + L1 + -1*R >= 0 && -3 + J + L1 >= 0 && -1*B1 + X >= 0 && B1 + -1*X >= 0 && K + -1*Z >= 0 && -1*K + Z >= 0 && -2 + B >= 0 && -2 + B + R >= 0 && -4 + B + J >= 0 && R >= 0 && -2 + J + R >= 0 && -2 + J >= 0 && D1 >= 0 && V1 >= 1 && O1 >= 2 && Z = X] f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True f18(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) -> exitus616(A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1) True Signature: {(exitus616,17);(f16,40);(f17,40);(f18,40);(f7,40);(f9,40)} Rule Graph: [0->{47},1->{46},2->{3,4,5,6,7,8},3->{45},4->{9,10,11,12,13,14,15,16},5->{9,10,11,12,13,14,15,16},6->{9,10 ,11,12,13,14,15,16},7->{9,10,11,12,13,14,15,16},8->{3,4,5,6,7,8},9->{9,10,11,12,13,14,15,16,17,18},10->{9,10 ,11,12,13,14,15,16,17,18},11->{9,10,11,12,13,14,15,16,17,18},12->{9,10,11,12,13,14,15,16,17,18},13->{9,10,11 ,12,13,14,15,16,17,18},14->{9,10,11,12,13,14,15,16,17,18},15->{9,10,11,12,13,14,15,16,17,18},16->{9,10,11,12 ,13,14,15,16,17,18},17->{19,20,21,22,23,24,25},18->{20,21,22,23,24,25,26},19->{19,20,21,22,23,24,25},20->{19 ,20,21,22,23,24,25,26,27,28},21->{19,20,21,22,23,24,25,26,27,28},22->{19,20,21,22,23,24,25,26,27,28},23->{19 ,20,21,22,23,24,25,26,27,28},24->{19,20,21,22,23,24,25,26,27,28},25->{19,20,21,22,23,24,25,26,27,28},26->{20 ,21,22,23,24,25,26},27->{30,32,34,36,38,40,42,44},28->{29,31,33,35,37,39,41,43}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47] | +- p:[8] c: [8] | +- p:[9,10,11,12,13,14,15,16] c: [9,10,11,12,13,14,15,16] | `- p:[19,20,21,22,23,24,25,26] c: [19,20,21,22,23,24,25,26]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1,0.0,0.1,0.2] f17 ~> f18 [A <= unknown, B <= unknown, C <= unknown, H <= unknown, I <= I, J <= K, K <= unknown, L <= unknown, M <= unknown, Q <= Q, R <= R, X <= unknown, Z <= unknown, B1 <= unknown, D1 <= D1, L1 <= L1, N1 <= N1] f17 ~> f18 [A <= unknown, B <= unknown, C <= unknown, H <= unknown, I <= I, J <= unknown, K <= K, L <= unknown, M <= K, Q <= Q, R <= R, X <= unknown, Z <= unknown, B1 <= unknown, D1 <= D1, L1 <= L1, N1 <= N1] f17 ~> f9 [A <= unknown, B <= 2*K, C <= unknown, H <= H, I <= I, J <= unknown, K <= unknown, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f9 ~> f18 [A <= unknown, B <= unknown, C <= unknown, H <= unknown, I <= I, J <= unknown, K <= C, L <= unknown, M <= C, Q <= Q, R <= R, X <= unknown, Z <= unknown, B1 <= unknown, D1 <= D1, L1 <= L1, N1 <= N1] f9 ~> f16 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= unknown, K <= K, L <= K, M <= unknown, Q <= K, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= K + R, N1 <= N1] f9 ~> f16 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= unknown, K <= K, L <= K, M <= unknown, Q <= K, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= K + R, N1 <= N1] f9 ~> f16 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= unknown, K <= K, L <= K, M <= unknown, Q <= K, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= K + R, N1 <= N1] f9 ~> f16 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= unknown, K <= K, L <= K, M <= unknown, Q <= K, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= K + R, N1 <= N1] f9 ~> f9 [A <= A, B <= A, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f7 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= unknown, K <= K, L <= unknown, M <= M, Q <= D1 + L1, R <= R, X <= M, Z <= K, B1 <= M, D1 <= D1, L1 <= L1, N1 <= 0*K] f16 ~> f7 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= unknown, K <= K, L <= unknown, M <= M, Q <= D1 + L1, R <= R, X <= M, Z <= K, B1 <= M, D1 <= D1, L1 <= L1, N1 <= 0*K] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= B1 + Z, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= B1 + Z, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f18 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= unknown, Z <= unknown, B1 <= unknown, D1 <= D1, L1 <= L1, N1 <= N1] f7 ~> f18 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= unknown, Z <= unknown, B1 <= unknown, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f18 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] + Loop: [0.0 <= K + A + B] f9 ~> f9 [A <= A, B <= A, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, Q <= Q, R <= R, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] + Loop: [0.1 <= R] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] f16 ~> f16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= L, L <= L, M <= unknown, Q <= J + Q, R <= L1, X <= X, Z <= Z, B1 <= B1, D1 <= D1, L1 <= L1, N1 <= N1] + Loop: [0.2 <= D1 + R] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= B1 + Z, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= unknown, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] f7 ~> f7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= unknown, K <= Z, L <= L, M <= B1 + Z, Q <= Q, R <= 0*K, X <= X, Z <= Z, B1 <= X, D1 <= D1 + L1, L1 <= L1, N1 <= N1] + Applied Processor: AbstractFlow + Details: () * Step 8: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,H,I,J,K,L,M,Q,R,X,Z,B1,D1,L1,N1,0.0,0.1,0.2] f17 ~> f18 [K ~=> J ,huge ~=> A ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> X ,huge ~=> Z] f17 ~> f18 [K ~=> M ,huge ~=> A ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> H ,huge ~=> J ,huge ~=> L ,huge ~=> X ,huge ~=> Z] f17 ~> f9 [K ~=> B,huge ~=> A,huge ~=> C,huge ~=> J,huge ~=> K] f9 ~> f18 [C ~=> K ,C ~=> M ,huge ~=> A ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> H ,huge ~=> J ,huge ~=> L ,huge ~=> X ,huge ~=> Z] f9 ~> f16 [C ~=> H ,K ~=> L ,R ~=> I ,K ~=> Q ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> J ,huge ~=> M ,R ~+> L1 ,K ~+> L1] f9 ~> f16 [C ~=> H ,K ~=> L ,R ~=> I ,K ~=> Q ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> J ,huge ~=> M ,R ~+> L1 ,K ~+> L1] f9 ~> f16 [C ~=> H ,K ~=> L ,R ~=> I ,K ~=> Q ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> J ,huge ~=> M ,R ~+> L1 ,K ~+> L1] f9 ~> f16 [C ~=> H ,K ~=> L ,R ~=> I ,K ~=> Q ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> J ,huge ~=> M ,R ~+> L1 ,K ~+> L1] f9 ~> f9 [A ~=> B,huge ~=> C] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f7 [K ~=> Z,M ~=> B1,M ~=> X,K ~=> N1,huge ~=> H,huge ~=> J,huge ~=> L,D1 ~+> Q,L1 ~+> Q] f16 ~> f7 [K ~=> Z,M ~=> B1,M ~=> X,K ~=> N1,huge ~=> H,huge ~=> J,huge ~=> L,D1 ~+> Q,L1 ~+> Q] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,B1 ~+> M,D1 ~+> D1,L1 ~+> D1,Z ~+> M] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,B1 ~+> M,D1 ~+> D1,L1 ~+> D1,Z ~+> M] f7 ~> f18 [huge ~=> B1,huge ~=> J,huge ~=> X,huge ~=> Z] f7 ~> f18 [huge ~=> B1,huge ~=> J,huge ~=> X,huge ~=> Z] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] f18 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f9 ~> f9 [A ~=> B,huge ~=> C] + Loop: [R ~=> 0.1] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] f16 ~> f16 [L ~=> K,L1 ~=> R,huge ~=> J,huge ~=> M,J ~+> Q,Q ~+> Q] + Loop: [D1 ~+> 0.2,R ~+> 0.2] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,B1 ~+> M,D1 ~+> D1,L1 ~+> D1,Z ~+> M] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,huge ~=> M,D1 ~+> D1,L1 ~+> D1] f7 ~> f7 [X ~=> B1,Z ~=> K,K ~=> R,huge ~=> J,B1 ~+> M,D1 ~+> D1,L1 ~+> D1,Z ~+> M] + Applied Processor: Lare + Details: Unknown bound. MAYBE