warning: Ignored call to f18/40 in equation f17/40 warning: Ignored call to f18/40 in equation f17/40 warning: Ignored call to f18/40 in equation f17/40 warning: Ignored call to f18/40 in equation f6/40 warning: Ignored call to f18/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f6/40 warning: Ignored call to loop_cont_f7/40 in equation f13/40 warning: Ignored call to loop_cont_f7/40 in equation f13/40 warning: Ignored call to loop_cont_f7/40 in equation f13/40 warning: Ignored call to loop_cont_f7/40 in equation loop_cont_f16/40 Warning: the following predicates are never called:[f13/40,f6/40] Inferred cost of 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3): 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[43]: 1 with precondition: [A=2,B=2,J=2,Q=1,O1=0,F2=1,C=E,U1=F,V1=G,H1=K,D2=O,E2=P,I2=T,J2=U,K2=V,L2=W,M2=X,N2=Y,O2=Z,P2=A1,Q2=B1,S2=D1,T2=E1,U2=F1,V2=G1,C=I1,Y2=J1,C3=N1,C=W1,R=X1,H1=Z1,H1=A2,B2=C2,R=G2,R+1=A3,Q1>=2,Y1>=2,H1>=C+1,B2>=H1+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[44]: 0 with precondition: [B=2,O1=1,Q1=2,S1=D,C=E,U1=F,V1=G,W1=H,X1=I,A=J,H1=K,A2=L,B2=M,C2=N,D2=O,E2=P,F2=Q,G2=R,H2=S,I2=T,J2=U,K2=V,L2=W,M2=X,N2=Y,O2=Z,P2=A1,Q2=B1,R2=C1,S2=D1,T2=E1,U2=F1,V2=G1,C=I1,Y2=J1,Z2=K1,A3=L1,B3=M1,C3=N1,A=P1,C=R1,C=T1,A=Y1,H1=Z1,H1=W2,C=X2,A>=2] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[45]: 1 with precondition: [A=2,B=2,J=2,Q=1,O1=0,F2=1,C=E,U1=F,V1=G,H1=K,D2=O,E2=P,I2=T,J2=U,K2=V,L2=W,M2=X,N2=Y,O2=Z,P2=A1,Q2=B1,S2=D1,T2=E1,U2=F1,V2=G1,C=I1,Y2=J1,C3=N1,C=W1,R=X1,H1=Z1,H1=A2,B2=C2,R=G2,R+1=A3,Q1>=2,Y1>=2,C>=H1+1,B2>=H1+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[46]: 1 with precondition: [A=2,B=2,J=2,Q=1,O1=0,F2=1,C=E,U1=F,V1=G,H1=K,D2=O,E2=P,I2=T,J2=U,K2=V,L2=W,M2=X,N2=Y,O2=Z,P2=A1,Q2=B1,S2=D1,T2=E1,U2=F1,V2=G1,C=I1,Y2=J1,C3=N1,C=W1,R=X1,H1=Z1,H1=A2,B2=C2,R=G2,R+1=A3,Q1>=2,Y1>=2,H1>=C+1,H1>=B2+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[47]: 1 with precondition: [A=2,B=2,J=2,Q=1,O1=0,F2=1,C=E,U1=F,V1=G,H1=K,D2=O,E2=P,I2=T,J2=U,K2=V,L2=W,M2=X,N2=Y,O2=Z,P2=A1,Q2=B1,S2=D1,T2=E1,U2=F1,V2=G1,C=I1,Y2=J1,C3=N1,C=W1,R=X1,H1=Z1,H1=A2,B2=C2,R=G2,R+1=A3,Q1>=2,Y1>=2,C>=H1+1,H1>=B2+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[48]: 1 with precondition: [A=2,B=2,J=2,O1=1,C=E,U1=F,V1=G,X1=I,C=K,D2=O,E2=P,F2=Q,G2=R,H2=S,I2=T,J2=U,K2=V,L2=W,N2=Y,S2=D1,T2=E1,U2=F1,V2=G1,C=H1,C=I1,Y2=J1,A3=L1,B3=M1,C3=N1,C=Z1,C=B2,Y1>=2,Q1>=Y1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[42],43]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*V1+ -1 with precondition: [Q=1,O1=0,F2=1,C=E,A=J,H1=K,A=V1+1,R=X1,H1=Z1,H1=A2,B2=C2,O=D2,P=E2,R=G2,T=I2,U=J2,V=K2,W=L2,X=M2,Y=N2,Z=O2,A1=P2,B1=Q2,D1=S2,E1=T2,F1=U2,G1=V2,J1=Y2,R+1=A3,N1=C3,B>=2,Q1>=2,Y1>=2,A>=B+1,B2>=H1+1,H1>=W1+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[42],44]: 0+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*P1+ -2,it1=<1*Q1+ -2,it1=<1*V1+ -1,it1=<1*Y1+ -2,it1=<1*V1+ -1*B+1 with precondition: [O1=1,C=E,A=J,K=H1,A=P1,V1+1=Q1,R1=T1,H=W1,I=X1,A=Y1,K=Z1,L=A2,M=B2,N=C2,O=D2,P=E2,Q=F2,R=G2,S=H2,T=I2,U=J2,V=K2,W=L2,X=M2,Y=N2,Z=O2,A1=P2,B1=Q2,C1=R2,D1=S2,E1=T2,F1=U2,G1=V2,K=W2,I1=X2,J1=Y2,K1=Z2,L1=A3,M1=B3,N1=C3,B>=2,V1>=B,A>=V1+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[42],45]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*V1+ -1 with precondition: [Q=1,O1=0,F2=1,C=E,A=J,H1=K,A=V1+1,R=X1,H1=Z1,H1=A2,B2=C2,O=D2,P=E2,R=G2,T=I2,U=J2,V=K2,W=L2,X=M2,Y=N2,Z=O2,A1=P2,B1=Q2,D1=S2,E1=T2,F1=U2,G1=V2,J1=Y2,R+1=A3,N1=C3,B>=2,Q1>=2,Y1>=2,A>=B+1,W1>=H1+1,B2>=H1+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[42],46]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*V1+ -1 with precondition: [Q=1,O1=0,F2=1,C=E,A=J,A2=K,A2=H1,A=V1+1,R=X1,A2=Z1,B2=C2,O=D2,P=E2,R=G2,T=I2,U=J2,V=K2,W=L2,X=M2,Y=N2,Z=O2,A1=P2,B1=Q2,D1=S2,E1=T2,F1=U2,G1=V2,J1=Y2,R+1=A3,N1=C3,B>=2,Q1>=2,Y1>=2,A>=B+1,A2>=W1+1,A2>=B2+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[42],47]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*V1+ -1 with precondition: [Q=1,O1=0,F2=1,C=E,A=J,H1=K,A=V1+1,R=X1,H1=Z1,H1=A2,B2=C2,O=D2,P=E2,R=G2,T=I2,U=J2,V=K2,W=L2,X=M2,Y=N2,Z=O2,A1=P2,B1=Q2,D1=S2,E1=T2,F1=U2,G1=V2,J1=Y2,R+1=A3,N1=C3,B>=2,Q1>=2,Y1>=2,A>=B+1,W1>=H1+1,H1>=B2+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[42],48]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*V1+ -1 with precondition: [O1=1,C=E,A=J,K=H1,A=V1+1,I=X1,K=Z1,K=B2,O=D2,P=E2,Q=F2,R=G2,S=H2,T=I2,U=J2,V=K2,W=L2,Y=N2,D1=S2,E1=T2,F1=U2,G1=V2,J1=Y2,L1=A3,M1=B3,N1=C3,B>=2,Y1>=2,A>=B+1,Q1>=Y1] Inferred cost of 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3): 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[58]: 0 with precondition: [O1=1,P1=A,Q1=B,R1=C,S1=D,T1=E,U1=F,V1=G,W1=H,X1=I,Y1=J,Z1=K,A2=L,B2=M,C2=N,D2=O,E2=P,F2=Q,G2=R,H2=S,I2=T,J2=U,K2=V,L2=W,M2=X,N2=Y,O2=Z,P2=A1,Q2=B1,R2=C1,S2=D1,T2=E1,U2=F1,V2=G1,W2=H1,X2=I1,Y2=J1,Z2=K1,A3=L1,B3=M1,C3=N1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[59]: 1 with precondition: [O1=0,C3=0,P1=A,Q1=B,R1=C,S1=D,T1=E,U1=F,V1=G,L=H,X1=I,D2=O,E2=P,H2=S,I2=T,J2=U,K2=V,L2=W,R2=C1,T2=E1,U2=F1,V2=G1,W2=H1,X2=I1,Y2=J1,Z2=K1,A3=L1,B3=M1,K=Z1,M=B2,R=G2,M=M2,K=O2,M=P2,M=Q2,D1=S2,F2+R=D1+1,N2+R=D1,Q>=0,R>=0,Y1>=2,K>=M+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[60]: 1 with precondition: [O1=0,C3=0,P1=A,Q1=B,R1=C,S1=D,T1=E,U1=F,V1=G,L=H,X1=I,D2=O,E2=P,H2=S,I2=T,J2=U,K2=V,L2=W,R2=C1,T2=E1,U2=F1,V2=G1,W2=H1,X2=I1,Y2=J1,Z2=K1,A3=L1,B3=M1,K=Z1,M=B2,R=G2,M=M2,K=O2,M=P2,M=Q2,D1=S2,F2+R=D1+1,N2+R=D1,Q>=0,R>=0,Y1>=2,M>=K+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[50,51,52,53,54,55,56,57],58]: 0+it1*(1) Such that:it1=<1*R+1,it1=<1*R+ -1*G2 with precondition: [O1=1,A=P1,B=Q1,C=R1,D=S1,E=T1,F=U1,G=V1,H=W1,I=X1,L=Z1,L=A2,B2=C2,O=D2,P=E2,H=I2,F2=K2,G2=L2,X=M2,Y=N2,Z=O2,A1=P2,B1=Q2,C1=R2,D1=S2,E1=T2,F1=U2,G1=V2,H1=W2,I1=X2,J1=Y2,K1=Z2,L1=A3,M1=B3,N1=C3,F2+G2=Q+R,Q>=0,Y1>=2,G2+1>=0,F2>=Q+1] 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,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[50,51,52,53,54,55,56,57],59]: 1+it1*(1) Such that:it1=<1*R+1,it1=<1*R+1*F2+ -1*D1+ -1 with precondition: [O1=0,C3=0,H=L,A=P1,B=Q1,C=R1,D=S1,E=T1,F=U1,G=V1,I=X1,H=Z1,O=D2,P=E2,H=I2,B2=M2,F2=N2+1,H=O2,B2=P2,B2=Q2,C1=R2,D1=S2,E1=T2,F1=U2,G1=V2,H1=W2,I1=X2,J1=Y2,K1=Z2,L1=A3,M1=B3,D1+1=F2+G2,D1+1=F2+L2,D1+K2+1=F2+Q+R,Q>=0,Y1>=2,H>=B2+1,D1+1>=F2,F2+R>=D1+2] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[50,51,52,53,54,55,56,57],60]: 1+it1*(1) Such that:it1=<1*R+1,it1=<1*R+1*F2+ -1*D1+ -1 with precondition: [O1=0,C3=0,H=L,A=P1,B=Q1,C=R1,D=S1,E=T1,F=U1,G=V1,I=X1,H=Z1,O=D2,P=E2,H=I2,B2=M2,F2=N2+1,H=O2,B2=P2,B2=Q2,C1=R2,D1=S2,E1=T2,F1=U2,G1=V2,H1=W2,I1=X2,J1=Y2,K1=Z2,L1=A3,M1=B3,D1+1=F2+G2,D1+1=F2+L2,D1+K2+1=F2+Q+R,Q>=0,Y1>=2,B2>=H+1,D1+1>=F2,F2+R>=D1+2] Inferred cost of f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3): f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[70]: 1 with precondition: [O1=1,P1=A,Q1=B,R1=C,S1=D,T1=E,U1=F,V1=G,W1=H,X1=I,Z1=K,A2=L,B2=M,C2=N,D2=O,E2=P,F2=Q,H2=S,I2=T,J2=U,K2=V,L2=W,Z=X,N2=Y,T2=E1,U2=F1,V2=G1,W2=H1,X2=I1,Y2=J1,Z2=K1,A3=L1,B3=M1,C3=N1,R=G2,D1=S2,R>=0,D1>=0,Y1>=2] f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[62,63,64,65,66,67,68,69],70]: inf with precondition: [O1=1,G2=0,T2=0,X=Z,A=P1,B=Q1,C=R1,D=S1,E=T1,F=U1,G=V1,H=W1,I=X1,X=Z1,L=A2,N=C2,O=D2,P=E2,Q=F2,T=I2,U=J2,V=K2,W=L2,Y=N2,S2=U2,G1=V2,H1=W2,I1=X2,J1=Y2,K1=Z2,L1=A3,M1=B3,N1=C3,D1>=0,Y1>=2,S2>=0,D1+R>=S2+1] f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3):[[62,63,64,65,66,67,68,69],71]...: inf with precondition: [1>=O1,D1>=0,O1>=0] Inferred cost of loop_cont_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): loop_cont_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):[72]: 1 with precondition: [Z=X,R>=0,D1>=0] loop_cont_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):[73]: inf with precondition: [Z=X,D1>=0,D1+R>=1] loop_cont_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):[74]...: inf with precondition: [D1>=0] loop_cont_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):[75]...: inf with precondition: [D1>=0] Inferred cost of loop_cont_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): loop_cont_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):[77]: 0 with precondition: [] loop_cont_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):[78]: 0+it1*(1) Such that:it1=<1*R+1 with precondition: [Q>=0,R>=0] loop_cont_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):[79]...: inf with precondition: [L=H,Q>=0,R>=0,D1>=0,K>=M+1] loop_cont_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):[80]...: inf with precondition: [L=H,Q>=0,R>=0,D1>=0,K>=M+1] loop_cont_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):[81]...: inf with precondition: [L=H,Q>=0,R>=0,D1>=0,M>=K+1] loop_cont_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):[82]...: inf with precondition: [L=H,Q>=0,R>=0,D1>=0,M>=K+1] loop_cont_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):[83]...: inf with precondition: [L=H,Q>=0,R>=1,D1>=0] loop_cont_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):[84]...: inf with precondition: [L=H,Q>=0,R>=1,D1>=0] loop_cont_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):[85]...: inf with precondition: [L=H,Q>=0,R>=1,D1>=0] loop_cont_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):[86]...: inf with precondition: [L=H,Q>=0,R>=1,D1>=0] Inferred cost of 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): 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):[88]: 1 with precondition: [] 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):[89]: 1 with precondition: [] 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):[90]: 2 with precondition: [Q=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):[91]: 2+it1*(1) Such that:it1=<1*R+1 with precondition: [Q=1,R>=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):[92]: 2 with precondition: [Q=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):[93]: 2+it1*(1) Such that:it1=<1*R+1 with precondition: [Q=1,R>=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):[94]: 2 with precondition: [Q=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):[95]: 2+it1*(1) Such that:it1=<1*R+1 with precondition: [Q=1,R>=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):[96]: 2 with precondition: [Q=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):[97]: 2+it1*(1) Such that:it1=<1*R+1 with precondition: [Q=1,R>=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):[98]: inf with precondition: [Q=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):[99]: inf with precondition: [Q=1,R>=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):[100]: inf with precondition: [Q=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):[101]: inf with precondition: [Q=1,R>=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):[102]: inf with precondition: [Q=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):[103]: inf with precondition: [Q=1,R>=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):[104]: inf with precondition: [Q=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):[105]: inf with precondition: [Q=1,R>=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):[106]: 1 with precondition: [] 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):[107]: 2 with precondition: [] 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):[108]: inf with precondition: [] 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):[109]: inf with precondition: [] Solved cost expressions of 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): 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):[88]: 1 with precondition: [] 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):[89]: 1 with precondition: [] 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):[90]: 2 with precondition: [Q=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):[91]: 1*R+3 with precondition: [Q=1,R>=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):[92]: 2 with precondition: [Q=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):[93]: 1*R+3 with precondition: [Q=1,R>=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):[94]: 2 with precondition: [Q=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):[95]: 1*R+3 with precondition: [Q=1,R>=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):[96]: 2 with precondition: [Q=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):[97]: 1*R+3 with precondition: [Q=1,R>=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):[98]: inf with precondition: [Q=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):[99]: inf with precondition: [Q=1,R>=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):[100]: inf with precondition: [Q=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):[101]: inf with precondition: [Q=1,R>=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):[102]: inf with precondition: [Q=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):[103]: inf with precondition: [Q=1,R>=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):[104]: inf with precondition: [Q=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):[105]: inf with precondition: [Q=1,R>=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):[106]: 1 with precondition: [] 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):[107]: 2 with precondition: [] 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):[108]: inf with precondition: [] 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):[109]: inf with precondition: [] Maximum cost of 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): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 420 ms. Invariants computed in 2179 ms. ----Backward Invariants 1163 ms. ----Transitive Invariants 390 ms. Refinement performed in 3741 ms. Termination proved in 1342 ms. Upper bounds computed in 771 ms. ----Phase cost structures 308 ms. --------Equation cost structures 301 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 432 ms. ----Solving cost expressions 2 ms. Compressed phase information: 10 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 10156 ms.