warning: Ignored call to f4/54 in equation f3/54 warning: Ignored call to f4/54 in equation f3/54 warning: Ignored call to f4/54 in equation f3/54 warning: Ignored call to f4/54 in equation f5/54 warning: Ignored call to f4/54 in equation f5/54 warning: Ignored call to f4/54 in equation f6/54 warning: Ignored call to f4/54 in equation f6/54 warning: Ignored call to f4/54 in equation f6/54 warning: Ignored call to f4/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f5/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation f6/54 warning: Ignored call to loop_cont_f7/54 in equation loop_cont_f1/54 Warning: the following predicates are never called:[f5/54,f6/54] Inferred cost of f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4): f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[37]: 1 with precondition: [A=2,B=2,M=0,N=2,C2=0,P2=0,C=E,I2=F,J2=G,K2=H,J=K,S1=O,W2=T,X2=U,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,U3=R1,C=U1,Y3=V1,E4=B2,I=L2,J=M2,J=N2,E1=O2,S1=R2,S1=S2,V2=T2,J=U2,V=Y2,J=F3,E1=H3,E1+1=Z3,V=A4,I=B4,Q2>=2,S1>=J+1,W1>=Q2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[38]: 0 with precondition: [B=2,C2=1,E2=2,G2=D,C=E,I2=F,J2=G,K2=H,L2=I,M2=J,N2=K,O2=L,P2=M,A=N,S1=O,S2=P,T2=Q,U2=R,V2=S,W2=T,X2=U,Y2=V,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,F3=C1,G3=D1,H3=E1,I3=F1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,U3=R1,W3=T1,C=U1,Y3=V1,Z3=W1,A4=X1,B4=Y1,C4=Z1,D4=A2,E4=B2,A=D2,C=F2,C=H2,A=Q2,S1=R2,S1=V3,C=X3,A>=2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[39]: 1 with precondition: [A=2,B=2,M=0,N=2,C2=0,P2=0,C=E,I2=F,J2=G,K2=H,J=K,S1=O,W2=T,X2=U,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,U3=R1,C=U1,Y3=V1,E4=B2,I=L2,J=M2,J=N2,E1=O2,S1=R2,S1=S2,V2=T2,J=U2,V=Y2,J=F3,E1=H3,E1+1=Z3,V=A4,I=B4,Q2>=2,J>=S1+1,W1>=Q2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[40]: 1 with precondition: [A=2,B=2,N=2,C2=1,C=E,I2=F,J2=G,K2=H,L2=I,O=J,N2=K,O2=L,P2=M,V2=S,W2=T,X2=U,Y2=V,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,H3=E1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,U3=R1,O=S1,C=U1,Y3=V1,A4=X1,B4=Y1,C4=Z1,D4=A2,E4=B2,O=R2,W1=Z3,Q2>=2,W1>=Q2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[36],37]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*N+ -2,it1=<1*N+ -1*B,it1=<1*J2+ -1 with precondition: [M=0,C2=0,P2=0,C=E,J=K,A=N,O=S1,A=J2+1,I=K2,I=L2,J=M2,J=N2,E1=O2,O=R2,O=S2,J=U2,T2=V2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,J=F3,D1=G3,E1=H3,G1=J3,H1=K3,I1=L3,J1=M3,K1=N3,L1=O3,M1=P3,N1=Q3,O1=R3,P1=S3,Q1=T3,R1=U3,V1=Y3,E1+1=Z3,V=A4,I=B4,B2=E4,B>=2,Q2>=2,A>=B+1,O>=J+1,W1>=Q2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[36],38]: 0+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*N+ -2,it1=<1*N+ -1*B,it1=<1*D2+ -2,it1=<1*E2+ -2,it1=<1*J2+ -1,it1=<1*Q2+ -2,it1=<1*J2+ -1*B+1 with precondition: [C2=1,C=E,A=N,O=S1,A=D2,J2+1=E2,F2=H2,I=K2,I=L2,J=M2,K=N2,L=O2,M=P2,A=Q2,O=R2,P=S2,Q=T2,R=U2,S=V2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,C1=F3,D1=G3,E1=H3,F1=I3,G1=J3,H1=K3,I1=L3,J1=M3,K1=N3,L1=O3,M1=P3,N1=Q3,O1=R3,P1=S3,Q1=T3,R1=U3,O=V3,T1=W3,U1=X3,V1=Y3,W1=Z3,X1=A4,Y1=B4,Z1=C4,A2=D4,B2=E4,B>=2,J2>=B,A>=J2+1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[36],39]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*N+ -2,it1=<1*N+ -1*B,it1=<1*J2+ -1 with precondition: [M=0,C2=0,P2=0,C=E,J=K,A=N,O=S1,A=J2+1,I=K2,I=L2,J=M2,J=N2,E1=O2,O=R2,O=S2,J=U2,T2=V2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,J=F3,D1=G3,E1=H3,G1=J3,H1=K3,I1=L3,J1=M3,K1=N3,L1=O3,M1=P3,N1=Q3,O1=R3,P1=S3,Q1=T3,R1=U3,V1=Y3,E1+1=Z3,V=A4,I=B4,B2=E4,B>=2,Q2>=2,A>=B+1,J>=O+1,W1>=Q2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[36],40]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*N+ -2,it1=<1*N+ -1*B,it1=<1*J2+ -1 with precondition: [C2=1,C=E,S1=J,A=N,S1=O,Z3=W1,A=J2+1,I=K2,I=L2,K=N2,L=O2,M=P2,S1=R2,S=V2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,D1=G3,E1=H3,G1=J3,H1=K3,I1=L3,J1=M3,K1=N3,L1=O3,M1=P3,N1=Q3,O1=R3,P1=S3,Q1=T3,R1=U3,V1=Y3,X1=A4,Y1=B4,Z1=C4,A2=D4,B2=E4,B>=2,Q2>=2,A>=B+1,Z3>=Q2] 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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4): 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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[58]: 1 with precondition: [C2=1,D2=A,E2=B,F2=C,G2=D,H2=E,I2=F,J2=G,K2=H,L2=I,P=J,O2=L,V2=S,W2=T,X2=U,Y2=V,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,V3=S1,W3=T1,X3=U1,Y3=V1,Z3=W1,A4=X1,B4=Y1,C4=Z1,D4=A2,E4=B2,K=N2,M=P2,E1=H3,M>=0,E1>=0,Q2>=2,R2>=K+1,R2>=U3+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[59]: 1 with precondition: [C2=1,D2=A,E2=B,F2=C,G2=D,H2=E,I2=F,J2=G,K2=H,L2=I,P=J,O2=L,V2=S,W2=T,X2=U,Y2=V,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,V3=S1,W3=T1,X3=U1,Y3=V1,Z3=W1,A4=X1,B4=Y1,C4=Z1,D4=A2,E4=B2,K=N2,M=P2,E1=H3,M>=0,E1>=0,Q2>=2,K>=R2+1,R2>=U3+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[60]: 1 with precondition: [C2=1,D2=A,E2=B,F2=C,G2=D,H2=E,I2=F,J2=G,K2=H,L2=I,P=J,O2=L,V2=S,W2=T,X2=U,Y2=V,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,V3=S1,W3=T1,X3=U1,Y3=V1,Z3=W1,A4=X1,B4=Y1,C4=Z1,D4=A2,E4=B2,K=N2,M=P2,E1=H3,M>=0,E1>=0,Q2>=2,R2>=K+1,U3>=R2+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[61]: 1 with precondition: [C2=1,D2=A,E2=B,F2=C,G2=D,H2=E,I2=F,J2=G,K2=H,L2=I,P=J,O2=L,V2=S,W2=T,X2=U,Y2=V,Z2=W,A3=X,B3=Y,C3=Z,D3=A1,E3=B1,G3=D1,J3=G1,K3=H1,L3=I1,M3=J1,N3=K1,O3=L1,P3=M1,Q3=N1,R3=O1,S3=P1,T3=Q1,V3=S1,W3=T1,X3=U1,Y3=V1,Z3=W1,A4=X1,B4=Y1,C4=Z1,D4=A2,E4=B2,K=N2,M=P2,E1=H3,M>=0,E1>=0,Q2>=2,K>=R2+1,U3>=R2+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57],58]: 1+it1*(1) Such that:it1=<1*E1+1,it1=<1*E1+ -1*H3 with precondition: [C2=1,J=P,A=D2,B=E2,C=F2,D=G2,E=H2,F=I2,G=J2,H=K2,I=L2,K=N2,L=O2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,D1=G3,G1=J3,H1=K3,I1=L3,J1=M3,V=P3,I=Q3,K=R3,P2=S3,H3=T3,S1=V3,T1=W3,U1=X3,V1=Y3,W1=Z3,X1=A4,Y1=B4,Z1=C4,A2=D4,B2=E4,H3+P2=E1+M,P2>=0,Q2>=2,H3>=0,R2>=K+1,E1>=H3+1,R2>=U3+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57],59]: 1+it1*(1) Such that:it1=<1*E1+1,it1=<1*E1+ -1*H3 with precondition: [C2=1,J=P,A=D2,B=E2,C=F2,D=G2,E=H2,F=I2,G=J2,H=K2,I=L2,K=N2,L=O2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,D1=G3,G1=J3,H1=K3,I1=L3,J1=M3,V=P3,I=Q3,K=R3,P2=S3,H3=T3,S1=V3,T1=W3,U1=X3,V1=Y3,W1=Z3,X1=A4,Y1=B4,Z1=C4,A2=D4,B2=E4,H3+P2=E1+M,P2>=0,Q2>=2,H3>=0,K>=R2+1,E1>=H3+1,R2>=U3+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57],60]: 1+it1*(1) Such that:it1=<1*E1+1,it1=<1*E1+ -1*H3 with precondition: [C2=1,J=P,A=D2,B=E2,C=F2,D=G2,E=H2,F=I2,G=J2,H=K2,I=L2,K=N2,L=O2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,D1=G3,G1=J3,H1=K3,I1=L3,J1=M3,V=P3,I=Q3,K=R3,P2=S3,H3=T3,S1=V3,T1=W3,U1=X3,V1=Y3,W1=Z3,X1=A4,Y1=B4,Z1=C4,A2=D4,B2=E4,H3+P2=E1+M,P2>=0,Q2>=2,H3>=0,R2>=K+1,U3>=R2+1,E1>=H3+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,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4,B4,C4,D4,E4):[[42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57],61]: 1+it1*(1) Such that:it1=<1*E1+1,it1=<1*E1+ -1*H3 with precondition: [C2=1,J=P,A=D2,B=E2,C=F2,D=G2,E=H2,F=I2,G=J2,H=K2,I=L2,K=N2,L=O2,T=W2,U=X2,V=Y2,W=Z2,X=A3,Y=B3,Z=C3,A1=D3,B1=E3,D1=G3,G1=J3,H1=K3,I1=L3,J1=M3,V=P3,I=Q3,K=R3,P2=S3,H3=T3,S1=V3,T1=W3,U1=X3,V1=Y3,W1=Z3,X1=A4,Y1=B4,Z1=C4,A2=D4,B2=E4,H3+P2=E1+M,P2>=0,Q2>=2,H3>=0,K>=R2+1,U3>=R2+1,E1>=H3+1] Inferred cost of loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2): loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[63]: 1 with precondition: [P=J,M>=0,E1>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[64]: 1 with precondition: [P=J,M>=0,E1>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[65]: 1 with precondition: [P=J,M>=0,E1>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[66]: 1 with precondition: [P=J,M>=0,E1>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[67]: 1+it1*(1) Such that:it1=<1*E1,it1=<1*E1+1 with precondition: [P=J,E1>=1,E1+M>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[68]: 1+it1*(1) Such that:it1=<1*E1,it1=<1*E1+1 with precondition: [P=J,E1>=1,E1+M>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[69]: 1+it1*(1) Such that:it1=<1*E1,it1=<1*E1+1 with precondition: [P=J,E1>=1,E1+M>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[70]: 1+it1*(1) Such that:it1=<1*E1,it1=<1*E1+1 with precondition: [P=J,E1>=1,E1+M>=0] Inferred cost of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2): f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[72]: 1 with precondition: [0>=N] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[73]: 1 with precondition: [N=1] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[74]: 1 with precondition: [N>=2] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[75]: 2 with precondition: [N=2,W1>=2] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[76]: 1+it1*(1) Such that:it1=<1*N+ -2 with precondition: [N>=3] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[77]: 2+it1*(1) Such that:it1=<1*N+ -2 with precondition: [N>=3,W1>=2] Solved cost expressions of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2): f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[72]: 1 with precondition: [0>=N] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[73]: 1 with precondition: [N=1] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[74]: 1 with precondition: [N>=2] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[75]: 2 with precondition: [N=2,W1>=2] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[76]: 1*N+ -1 with precondition: [N>=3] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2):[77]: 1*N with precondition: [N>=3,W1>=2] Maximum cost of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2): max([1*N,2]) Asymptotic class: n Time statistics: Partial evaluation computed in 618 ms. Invariants computed in 4033 ms. ----Backward Invariants 2405 ms. ----Transitive Invariants 658 ms. Refinement performed in 6182 ms. Termination proved in 2694 ms. Upper bounds computed in 807 ms. ----Phase cost structures 283 ms. --------Equation cost structures 270 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 490 ms. ----Solving cost expressions 1 ms. Compressed phase information: 9 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 17415 ms.