warning: Ignored call to loop_cont_f5/27 in equation loop_cont_f9/27 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): 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):[29]: 0 with precondition: [A=17,B=1,C=0,B1=1,C1=17,D1=1,E1=0,D=E,D=F,I1=G,J1=H,K1=I,L1=J,M1=K,N1=L,O1=M,P1=N,Q1=O,R1=P,S1=Q,T1=R,U1=S,V1=T,W1=U,X1=V,Y1=W,Z1=X,A2=Y,B2=Z,C2=A1,D=F1,D=G1,D=H1] 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):[[27],28]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,C>=0,F1>=1,J1>=1,T1>=1,B2>=C2] 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):[[27],29]: 0+it1*(1) Such that:it1=<16,it1=<1*E1,it1=<-1*B+17,it1=<-1*C+16,it1=<1*D1+ -1,it1=<1*E1+ -1*C,it1=<1*E1+ -1*B+1 with precondition: [A=17,B1=1,C1=17,C+1=B,D=E,D=F,E1+1=D1,F1=G1,F1=H1,G=I1,H=J1,I=K1,J=L1,K=M1,L=N1,M=O1,N=P1,O=Q1,P=R1,Q=S1,R=T1,S=U1,T=V1,U=W1,V=X1,W=Y1,X=Z1,Y=A2,Z=B2,A1=C2,16>=E1,C>=0,E1>=C+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):[[27],30]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=F1+1,C>=0,J1>=1,T1>=1,B2>=C2] 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):[[27],31]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=J1+1,C>=0,F1>=1,T1>=1,B2>=C2] 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):[[27],32]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=F1+1,0>=J1+1,C>=0,T1>=1,B2>=C2] 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):[[27],33]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=T1+1,C>=0,F1>=1,J1>=1,B2>=C2] 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):[[27],34]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=F1+1,0>=T1+1,C>=0,J1>=1,B2>=C2] 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):[[27],35]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=J1+1,0>=T1+1,C>=0,F1>=1,B2>=C2] 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):[[27],36]: 1+it1*(1) Such that:it1=<16,it1=<-1*B+17,it1=<-1*C+16 with precondition: [A=17,B1=0,C1=17,D1=17,E1=16,I1=13,K1=1,L1=0,V1=1,W1=13,A2=14,C+1=B,D=E,D=F,F1=G1,F1=H1,M=O1,N=P1,O=Q1,J1=S1,V=X1,F1=Y1,F1=Z1,15>=C,0>=F1+1,0>=J1+1,0>=T1+1,C>=0,B2>=C2] Inferred cost of f5(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): f5(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):[42]: 1 with precondition: [B1=1,C1=A,D1=B,E1=C,F1=D,G1=E,H1=F,R1=P,S1=Q,T1=R,U1=S,V1=T,W1=U,X1=V,Y1=W,Z1=X,A2=Y,B2=Z,C2=A1,G=I1,I=K1,H=L1,G>=0,H>=1,I>=1,P1>=O1+1] f5(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):[43]: 1 with precondition: [B1=1,C1=A,D1=B,E1=C,F1=D,G1=E,H1=F,R1=P,S1=Q,T1=R,U1=S,V1=T,W1=U,X1=V,Y1=W,Z1=X,A2=Y,B2=Z,C2=A1,G=I1,I=K1,H=L1,0>=H+1,G>=0,I>=1,P1>=O1+1] f5(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):[44]: 1 with precondition: [J=0,P=0,B1=1,L1=0,R1=0,C1=A,D1=B,E1=C,F1=D,G1=E,H1=F,Q1=O,U1=S,V1=T,W1=U,Z1=X,A2=Y,B2=Z,C2=A1,G=I1,H=J1,I=K1,M=O1,R=S1,R=T1,I=X1,G>=0,H>=1,I>=0,M>=P1] f5(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):[45]: 1 with precondition: [J=0,P=0,B1=1,L1=0,R1=0,C1=A,D1=B,E1=C,F1=D,G1=E,H1=F,Q1=O,U1=S,V1=T,W1=U,Z1=X,A2=Y,B2=Z,C2=A1,G=I1,H=J1,I=K1,M=O1,R=S1,R=T1,I=X1,0>=H+1,G>=0,I>=0,M>=P1] f5(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):[[38,39,40,41],42]: 1+it1*(1) Such that:it1=<1*G+1,it1=<1*G+ -1*I1 with precondition: [J=0,B1=1,A=C1,B=D1,C=E1,D=F1,E=G1,F=H1,W1=I1,X1+1=K1,L1=S1,X1+1=V1,W=Y1,X=Z1,Y=A2,Z=B2,A1=C2,W1+X1+1=G+I,L1>=1,W1>=0,P1>=O1+1,G>=W1+1,W1+X1+1>=G] f5(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):[[38,39,40,41],43]: 1+it1*(1) Such that:it1=<1*G+1,it1=<1*G+ -1*I1 with precondition: [J=0,B1=1,A=C1,B=D1,C=E1,D=F1,E=G1,F=H1,W1=I1,X1+1=K1,L1=S1,X1+1=V1,W=Y1,X=Z1,Y=A2,Z=B2,A1=C2,W1+X1+1=G+I,0>=L1+1,W1>=0,P1>=O1+1,G>=W1+1,W1+X1+1>=G] f5(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):[[38,39,40,41],44]: 1+it1*(1) Such that:it1=<1*G+1,it1=<1*G+ -1*I1 with precondition: [J=0,B1=1,L1=0,R1=0,A=C1,B=D1,C=E1,D=F1,E=G1,F=H1,X1=K1,M=O1,O=Q1,S1=T1,X1=V1,X=Z1,Y=A2,Z=B2,A1=C2,G+I=I1+X1,G+I=W1+X1,I>=0,J1>=1,X1>=I+1,M>=P1,G+I>=X1] f5(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):[[38,39,40,41],45]: 1+it1*(1) Such that:it1=<1*G+1,it1=<1*G+ -1*I1 with precondition: [J=0,B1=1,L1=0,R1=0,A=C1,B=D1,C=E1,D=F1,E=G1,F=H1,X1=K1,M=O1,O=Q1,S1=T1,X1=V1,X=Z1,Y=A2,Z=B2,A1=C2,G+I=I1+X1,G+I=W1+X1,0>=J1+1,I>=0,X1>=I+1,M>=P1,G+I>=X1] 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): 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):[47]: 1 with precondition: [G>=0,H>=1,I>=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):[48]: 1 with precondition: [0>=H+1,G>=0,I>=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):[49]: 1 with precondition: [J=0,P=0,G>=0,H>=1,I>=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):[50]: 1 with precondition: [J=0,P=0,0>=H+1,G>=0,I>=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):[51]: 1+it1*(1) Such that:it1=<1*G,it1=<1*G+1 with precondition: [J=0,G>=1,I>=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):[52]: 1+it1*(1) Such that:it1=<1*G,it1=<1*G+1 with precondition: [J=0,G>=1,I>=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):[53]: 1+it1*(1) Such that:it1=<1*G,it1=<1*G+1 with precondition: [J=0,G>=1,I>=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):[54]: 1+it1*(1) Such that:it1=<1*G,it1=<1*G+1 with precondition: [J=0,G>=1,I>=0] Inferred cost of f6(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): f6(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):[56]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[57]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[58]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[59]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[60]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[61]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[62]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[63]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[64]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[65]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[66]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[67]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[68]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[69]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[70]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[71]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[72]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[73]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[74]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[75]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[76]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[77]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[78]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[79]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[80]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[81]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[82]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[83]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[84]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[85]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[86]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[87]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[88]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[89]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[90]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[91]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[92]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[93]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[94]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[95]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[96]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[97]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[98]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[99]: 3+it1*(1) Such that:it1=<16 with precondition: [] f6(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):[100]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[101]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[102]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[103]: 3+it1*(1)+it2*(1) Such that:it1=<16,it2=<13,it2=<14 with precondition: [] f6(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):[104]: 1 with precondition: [] f6(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):[105]: 1+it1*(1) Such that:it1=<16 with precondition: [] Solved cost expressions of f6(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): f6(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):[56]: 19 with precondition: [] f6(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):[57]: 19 with precondition: [] f6(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):[58]: 32 with precondition: [] f6(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):[59]: 32 with precondition: [] f6(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):[60]: 32 with precondition: [] f6(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):[61]: 32 with precondition: [] f6(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):[62]: 19 with precondition: [] f6(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):[63]: 19 with precondition: [] f6(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):[64]: 32 with precondition: [] f6(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):[65]: 32 with precondition: [] f6(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):[66]: 32 with precondition: [] f6(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):[67]: 32 with precondition: [] f6(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):[68]: 19 with precondition: [] f6(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):[69]: 19 with precondition: [] f6(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):[70]: 32 with precondition: [] f6(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):[71]: 32 with precondition: [] f6(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):[72]: 32 with precondition: [] f6(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):[73]: 32 with precondition: [] f6(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):[74]: 19 with precondition: [] f6(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):[75]: 19 with precondition: [] f6(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):[76]: 32 with precondition: [] f6(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):[77]: 32 with precondition: [] f6(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):[78]: 32 with precondition: [] f6(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):[79]: 32 with precondition: [] f6(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):[80]: 19 with precondition: [] f6(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):[81]: 19 with precondition: [] f6(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):[82]: 32 with precondition: [] f6(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):[83]: 32 with precondition: [] f6(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):[84]: 32 with precondition: [] f6(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):[85]: 32 with precondition: [] f6(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):[86]: 19 with precondition: [] f6(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):[87]: 19 with precondition: [] f6(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):[88]: 32 with precondition: [] f6(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):[89]: 32 with precondition: [] f6(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):[90]: 32 with precondition: [] f6(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):[91]: 32 with precondition: [] f6(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):[92]: 19 with precondition: [] f6(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):[93]: 19 with precondition: [] f6(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):[94]: 32 with precondition: [] f6(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):[95]: 32 with precondition: [] f6(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):[96]: 32 with precondition: [] f6(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):[97]: 32 with precondition: [] f6(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):[98]: 19 with precondition: [] f6(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):[99]: 19 with precondition: [] f6(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):[100]: 32 with precondition: [] f6(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):[101]: 32 with precondition: [] f6(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):[102]: 32 with precondition: [] f6(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):[103]: 32 with precondition: [] f6(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):[104]: 1 with precondition: [] f6(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):[105]: 17 with precondition: [] Maximum cost of f6(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): 32 Asymptotic class: constant Time statistics: Partial evaluation computed in 106 ms. Invariants computed in 760 ms. ----Backward Invariants 519 ms. ----Transitive Invariants 69 ms. Refinement performed in 843 ms. Termination proved in 222 ms. Upper bounds computed in 656 ms. ----Phase cost structures 261 ms. --------Equation cost structures 255 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 368 ms. ----Solving cost expressions 5 ms. Compressed phase information: 14 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 2811 ms.