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