warning: Ignored call to f16/38 in equation f15/38 warning: Ignored call to f16/38 in equation f7/38 warning: Ignored call to f16/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f7/38 warning: Ignored call to loop_cont_f8/38 in equation f11/38 warning: Ignored call to loop_cont_f8/38 in equation f11/38 warning: Ignored call to loop_cont_f8/38 in equation f11/38 warning: Ignored call to loop_cont_f8/38 in equation loop_cont_f14/38 Warning: the following predicates are never called:[f10/38,f11/38,f7/38] 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): 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):[35]: 1 with precondition: [A=2,B=2,E=0,F=2,M1=0,R1=0,J=C,J=I,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,Y2=L1,D=N1,D=Q1,J=Y1,J=Z1,J=A2,0>=J+1,S1>=2,D>=S1,B2>=S1] 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):[36]: 0 with precondition: [A=2,M1=1,N1=2,J=C,Q1=D,R1=E,B=F,T1=G,U1=H,J=I,X1=K,Y1=L,Z1=M,A2=N,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,Y2=L1,B=O1,J=P1,B=S1,J=V1,J=W1,B>=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):[37]: 1 with precondition: [A=2,B=2,E=0,F=2,M1=0,R1=0,J=C,J=I,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,Y2=L1,D=N1,D=Q1,J=Y1,J=Z1,J=A2,J>=1,S1>=2,D>=S1,B2>=S1] 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):[[34],35]: 1+it1*(1) Such that:it1=<1*B+ -2,it1=<1*F+ -2,it1=<1*D2+ -1,it1=<1*D2+ -1*A+1 with precondition: [E=0,M1=0,R1=0,B=F,C=J,D=N1,D=Q1,Z1=Y1,Z1=A2,B=D2+1,R=E2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Y=L2,Z=M2,A1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,L1=Y2,0>=Z1+1,A>=2,S1>=2,B>=A+1,D>=S1,B2>=S1] 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):[[34],36]: 0+it1*(1) Such that:it1=<1*B+ -2,it1=<1*F+ -2,it1=<1*F+ -1*A,it1=<1*N1+ -2,it1=<1*O1+ -2,it1=<1*S1+ -2,it1=<1*D2+ -1,it1=<1*D2+ -1*A+1 with precondition: [M1=1,B=F,C=J,B=O1,D=Q1,E=R1,B=S1,G=T1,H=U1,I=V1,P1=W1,L=Y1,M=Z1,N=A2,O=B2,N1=D2+1,R=E2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Y=L2,Z=M2,A1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,L1=Y2,A>=2,N1>=A+1,B>=N1] 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):[[34],37]: 1+it1*(1) Such that:it1=<1*B+ -2,it1=<1*F+ -2,it1=<1*D2+ -1,it1=<1*D2+ -1*A+1 with precondition: [E=0,M1=0,R1=0,B=F,C=J,D=N1,D=Q1,A2=Y1,A2=Z1,B=D2+1,R=E2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Y=L2,Z=M2,A1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,L1=Y2,A>=2,S1>=2,A2>=1,B>=A+1,D>=S1,B2>=S1] Inferred cost of f14(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): f14(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):[43]: 0 with precondition: [M1=1,N1=A,O1=B,P1=C,Q1=D,R1=E,S1=F,T1=G,U1=H,V1=I,W1=J,X1=K,Y1=L,Z1=M,A2=N,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,Y2=L1] f14(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):[44]: 1 with precondition: [N=0,M1=0,Q2=0,S2=0,N1=A,O1=B,P1=C,T1=G,U1=H,V1=I,W1=J,X1=K,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,W2=J1,X2=K1,Y2=L1,D=Q1,I1+1=R1,L=Y1,L=O2,I1=P2,L=R2,L=T2,L=U2,I1=V2,D>=0,E>=0,L>=1,S1>=2] f14(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):[45]: 1 with precondition: [N=0,M1=0,Q2=0,S2=0,N1=A,O1=B,P1=C,T1=G,U1=H,V1=I,W1=J,X1=K,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,W2=J1,X2=K1,Y2=L1,D=Q1,I1+1=R1,L=Y1,L=O2,I1=P2,L=R2,L=T2,L=U2,I1=V2,0>=L+1,D>=0,E>=0,S1>=2] f14(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):[[39,40,41,42],43]: 0+it1*(1) Such that:it1=<1*D+1,it1=<1*D+ -1*Q1 with precondition: [M1=1,A=N1,B=O1,C=P1,G=T1,H=U1,I=V1,J=W1,K=X1,Y1=Z1,N=A2,O=B2,P=C2,Q=D2,S=F2,T=G2,U=H2,V=I2,W=J2,N=K2,Q1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,L1=Y2,Q1+R1=D+E,M2+Q1=D+E,E>=0,Q1+1>=0,S1>=2,D>=Q1+1] f14(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):[[39,40,41,42],44]: 1+it1*(1) Such that:it1=<1*D+1,it1=<1*D+ -1*Q1 with precondition: [N=0,M1=0,K2=0,Q2=0,S2=0,A=N1,B=O1,C=P1,I1+1=R1,G=T1,H=U1,I=V1,J=W1,K=X1,R2=Y1,O=B2,P=C2,Q=D2,S=F2,T=G2,U=H2,V=I2,W=J2,R2=O2,I1=P2,R2=T2,R2=U2,I1=V2,J1=W2,K1=X2,L1=Y2,D+E=M2+Q1,D+E=M2+N2,E>=0,S1>=2,R2>=1,M2>=E+1,D+E>=M2] f14(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):[[39,40,41,42],45]: 1+it1*(1) Such that:it1=<1*D+1,it1=<1*D+ -1*Q1 with precondition: [N=0,M1=0,K2=0,Q2=0,S2=0,A=N1,B=O1,C=P1,I1+1=R1,G=T1,H=U1,I=V1,J=W1,K=X1,R2=Y1,O=B2,P=C2,Q=D2,S=F2,T=G2,U=H2,V=I2,W=J2,R2=O2,I1=P2,R2=T2,R2=U2,I1=V2,J1=W2,K1=X2,L1=Y2,D+E=M2+Q1,D+E=M2+N2,0>=R2+1,E>=0,S1>=2,M2>=E+1,D+E>=M2] Inferred cost of f8(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): f8(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):[55]: 1 with precondition: [M1=1,N1=A,O1=B,P1=C,Q1=D,R1=E,T1=G,V1=I,W1=J,X1=K,Y1=L,Z1=M,A2=N,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,D1=B1,P2=C1,W2=J1,X2=K1,Y2=L1,I1=V2,I1>=0,S1>=2] f8(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):[[47,48,49,50,51,52,53,54],55]: 1+it1*(1) Such that:it1=<1*I1+1,it1=<1*I1+ -1*V2 with precondition: [B1=0,D1=0,M1=1,A=N1,B=O1,C=P1,D=Q1,E=R1,G=T1,I=V1,J=W1,K=X1,M=Z1,N=A2,O=B2,P=C2,Q=D2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Y=L2,Z=M2,A1=N2,C1=P2,V2=W2,K1=X2,L1=Y2,S1>=2,V2>=0,I1>=V2+1] Inferred cost of loop_cont_f14(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): loop_cont_f14(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):[57]: 1 with precondition: [D1=B1,I1>=0] loop_cont_f14(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):[58]: 1+it1*(1) Such that:it1=<1*I1,it1=<1*I1+1 with precondition: [B1=0,D1=0,I1>=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): 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):[60]: 0 with precondition: [] 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):[61]: 0+it1*(1) Such that:it1=<1*D+1 with precondition: [D>=0,E>=0] Inferred cost of f15(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): f15(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):[63]: 1 with precondition: [] f15(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):[64]: 2 with precondition: [E=0,D>=2] f15(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):[65]: 2+it1*(1) Such that:it1=<1*D+1 with precondition: [E=0,D>=2] f15(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):[66]: 2 with precondition: [E=0,D>=2] f15(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):[67]: 2+it1*(1) Such that:it1=<1*D+1 with precondition: [E=0,D>=2] f15(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):[68]: inf with precondition: [E=0,D>=2] f15(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):[69]: inf with precondition: [E=0,D>=2] f15(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):[70]: inf with precondition: [E=0,D>=2] f15(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):[71]: inf with precondition: [E=0,D>=2] f15(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):[72]: 1 with precondition: [] f15(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):[73]: inf with precondition: [] Solved cost expressions of f15(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): f15(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):[63]: 1 with precondition: [] f15(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):[64]: 2 with precondition: [E=0,D>=2] f15(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):[65]: 1*D+3 with precondition: [E=0,D>=2] f15(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):[66]: 2 with precondition: [E=0,D>=2] f15(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):[67]: 1*D+3 with precondition: [E=0,D>=2] f15(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):[68]: inf with precondition: [E=0,D>=2] f15(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):[69]: inf with precondition: [E=0,D>=2] f15(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):[70]: inf with precondition: [E=0,D>=2] f15(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):[71]: inf with precondition: [E=0,D>=2] f15(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):[72]: 1 with precondition: [] f15(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):[73]: inf with precondition: [] Maximum cost of f15(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): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 324 ms. Invariants computed in 1410 ms. ----Backward Invariants 639 ms. ----Transitive Invariants 298 ms. Refinement performed in 2521 ms. Termination proved in 1137 ms. Upper bounds computed in 463 ms. ----Phase cost structures 172 ms. --------Equation cost structures 162 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 267 ms. ----Solving cost expressions 0 ms. Compressed phase information: 6 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 7456 ms.