warning: Ignored call to loop_cont_f80/13 in equation loop_cont_f66/13 Inferred cost of f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f19(A,B,C,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]: 1 with precondition: [D=0,E=0,N=0,R=0,S=0,O=A,T=F,U=G,V=H,W=I,X=J,Y=K,Z=L,A1=M,B=P,C+1=Q,0>=B+1,B>=C] f19(A,B,C,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]: 0 with precondition: [B=1,D=0,E=0,N=1,P=1,R=0,S=0,O=A,T=F,U=G,V=H,W=I,X=J,Y=K,Z=L,A1=M,C=Q,1>=C] f19(A,B,C,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],61]: 1+it1*(1) Such that:it1=<1*S,it1=<-1*Q+1*S,it1=<1*P+1,it1=<1*S+ -1*E,it1=<-1*C+1*S+ -1,it1=<-1*Q+1*P+1,it1=<1*B+ -1*E+1 with precondition: [N=0,A=O,B=P,C+1=Q,B+1=S,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1,E>=0,E>=C+1,B>=E] f19(A,B,C,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],62]: 0+it1*(1) Such that:it1=<1,it1=<2 with precondition: [B=1,E=0,N=1,P=1,S=1,A=O,C=Q,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1,0>=C+1] f19(A,B,C,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],60,[58],61]: 2+it1*(1)+it2*(1) Such that:it1=<1*B+ -1,it1=<1*B+ -1*C,it1=<1*P+ -1,it1=<1*S+ -2,it1=<1*S+ -1*Q,it1=<-1*E+1*S+ -2,it1=<1*P+ -1*Q+1,it1=<1*S+ -1*C+ -1,it2=<1*P,it2=<1*B+ -1,it2=<1*B+ -1*E,it2=<1*C+ -1*E,it2=<1*P+ -1,it2=<1*Q+ -1,it2=<1*S+ -2,it2=<1*S+ -1,it2=<1*Q+ -1*E+ -1,it2=<1*S+ -1*E+ -1 with precondition: [N=0,A=O,B=P,C+1=Q,B+1=S,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1,E>=0,B>=C+1,C>=E+1] f19(A,B,C,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],60,61]: 2+it1*(1) Such that:it1=<1*P,it1=<1*B+ -1*E,it1=<1*C+ -1*E,it1=<1*Q+ -1,it1=<1*S+ -1,it1=<1*S+ -1*E+ -1 with precondition: [N=0,S=B+1,S=C+1,A=O,S=P+1,S=Q,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1,E>=0,S>=E+2] f19(A,B,C,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],62]: 0+it1*(1) Such that:it1=<1 with precondition: [B=1,C=1,E=0,N=1,P=1,Q=1,S=1,A=O,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1] f19(A,B,C,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,[58],61]: 2+it1*(1) Such that:it1=<1*B,it1=<1*P,it1=<1*S+ -1 with precondition: [C=0,D=0,E=0,N=0,Q=1,A=O,B=P,B+1=S,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1,B>=1] f19(A,B,C,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,61]: 2 with precondition: [B=0,C=0,D=0,E=0,N=0,P=0,Q=1,S=1,A=O,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1] f19(A,B,C,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,62]: 1 with precondition: [B=1,C=0,D=0,E=0,N=1,P=1,Q=0,S=1,A=O,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1] 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): 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):[68,[66],67,74]: 7+it1*(1)+it2*(3+it3*(1))+it4*(1)+it5*(1) Such that:it1=<5,it2=<4,it4=<19,it5=<5 it3=<5,it3=<4 with precondition: [A=50,B=5,C=0,N=0,O=50,P=5,Q=6,S=6,T=5,U=0,A1=50,H=V,I=W,J=X,K=Y,L=Z] Inferred cost of f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f41(A,B,C,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]: 1 with precondition: [J=0,N=0,X=0,O=A,P=B,Q=C,R=D,S=E,W=I,Y=K,Z=L,A1=M,F=T,G=U,H+1=V,0>=G,F>=H] f41(A,B,C,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],77]: 1+it1*(1) Such that:it1=<1*U,it1=<1*X,it1=<1*G+ -1*J,it1=<1*U+ -1*J with precondition: [N=0,X=G,A=O,B=P,C=Q,D=R,E=S,F=T,X=U,H+1=V,K=Y,L=Z,M=A1,J>=0,F>=H,X>=J+1] Inferred cost of f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f36(A,B,C,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]: 0 with precondition: [F=1,N=1,T=1,O=A,P=B,Q=C,R=D,S=E,G+1=H,W=I,X=J,Y=K,Z=L,A1=M,G=U,G+1=V,0>=G] f36(A,B,C,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],82]: 1+it1*(1) Such that:it1=<1*T,it1=<1*F+ -1*H+1,it1=<1*T+ -1*H+1 with precondition: [G=0,N=0,U=0,V=1,A=O,B=P,C=Q,D=R,E=S,F=T,J=X,K=Y,L=Z,M=A1,H>=1,F>=H] f36(A,B,C,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],82]: 1+it1*(2) Such that:it1=<-1*G+1*T,it1=<-1*V+1*T+1,it1=<1*F+ -1*H+1,it1=<1*T+ -1*H+1 with precondition: [N=0,X=0,U=G,A=O,B=P,C=Q,D=R,E=S,F=T,U+1=V,K=Y,L=Z,M=A1,0>=U+1,F>=H,H>=U+1] f36(A,B,C,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],83]: 0+it1*(2) Such that:it1=<-1*G+1,it1=<-1*H+2,it1=<-1*U+1,it1=<1*V+ -1*H,it1=<-1*G+1*V+ -1,it1=<-1*U+1*V+ -1 with precondition: [F=1,N=1,T=1,X=0,A=O,B=P,C=Q,D=R,E=S,G=U,K=Y,L=Z,M=A1,1>=V,H>=G+1,V>=H+1] f36(A,B,C,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],82]: 1+it1*(2+it2*(1)) Such that:it1=<-1*G+1*T,it1=<-1*X+1*T,it1=<1*F+ -1*H+1,it1=<1*T+ -1*H+1 it2=<1*F+ -1,it2=<1*G with precondition: [N=0,V=G+1,A=O,B=P,C=Q,D=R,E=S,F=T,V=U+1,V=X+1,K=Y,L=Z,M=A1,V>=2,F>=H,H>=V] Inferred cost of f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f54(A,B,C,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]: 1 with precondition: [J=0,N=0,X=0,O=A,P=B,Q=C,R=D,S=E,W=I,Y=K,Z=L,A1=M,F=T,G=U,H+1=V,0>=G+1,F>=H] f54(A,B,C,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],86]: 1+it1*(1) Such that:it1=<1*X,it1=<1*U+1,it1=<1*G+ -1*J+1,it1=<1*U+ -1*J+1 with precondition: [N=0,X=G+1,A=O,B=P,C=Q,D=R,E=S,F=T,X=U+1,H+1=V,K=Y,L=Z,M=A1,J>=0,F>=H,X>=J+1] Inferred cost of f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f50(A,B,C,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]: 1 with precondition: [N=0,O=A,P=B,Q=C,R=D,S=E,U=G+1,W=I,X=J,Y=K,Z=L,A1=M,F=T,H=V,H>=F+1] f50(A,B,C,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],90]: 1+it1*(2) Such that:it1=<1*F+ -1*H+1,it1=<1*T+ -1*H+1 with precondition: [N=0,X=0,A=O,B=P,C=Q,D=R,E=S,F=T,G+1=U,F+1=V,K=Y,L=Z,M=A1,0>=G+1,F>=H] f50(A,B,C,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],90]: 1+it1*(2+it2*(1)) Such that:it1=<1*F+ -1*H+1,it1=<1*T+ -1*H+1 it2=<1*G+1 with precondition: [N=0,A=O,B=P,C=Q,D=R,E=S,F=T,G+1=U,F+1=V,G+1=X,K=Y,L=Z,M=A1,G>=0,F>=H] Inferred cost of f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f33(A,B,C,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]: 1 with precondition: [F=1,N=1,0>=G] f33(A,B,C,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]: 1+it1*(2) Such that:it1=<-1*G,it1=<-1*G+1 with precondition: [F=1,N=1,0>=G+1] f33(A,B,C,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]: 1 with precondition: [N=0,U=1,O=A,P=B,Q=C,R=D,S=E,V=H,W=I,X=J,Y=K,Z=L,A1=M,F=T,G>=F] f33(A,B,C,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],92,[94],97]: 4+it1*(3+it2*(2+it3*(1))+it4*(2+it5*(1)))+it6*(1)+it7*(2+it8*(1))+it9*(3+it10*(2)+it11*(2)) Such that:it1=<1*F+ -1,it1=<1*T+ -1,it1=<1*V+ -2,it1=<1*X+ -1,it6=<1*F,it6=<1*T,it6=<1*X,it6=<1*V+ -1,it7=<1*F,it7=<1*T,it7=<1*X,it7=<1*V+ -1,it9=<-1*G,it9=<1*X+ -1*G it4=<1*F+ -1,it2=<1*F+ -1 it3=<1*F+ -1 it5=<1*F it8=<1 it11=<-1*G+1*F,it10=<-1*G+1*F with precondition: [N=0,U=1,A=O,B=P,C=Q,D=R,E=S,F=T,F+1=V,F=X,K=Y,L=Z,M=A1,0>=G+1,F>=2] f33(A,B,C,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],92,97]: 4+it1*(1)+it2*(2+it3*(1))+it4*(3+it5*(2)+it6*(2)) Such that:it1=<1,it2=<1,it4=<-1*G,it4=<-1*G+1 it3=<1 it6=<-1*G+1*F,it5=<-1*G+1*F with precondition: [F=1,N=0,T=1,U=1,V=2,X=1,A=O,B=P,C=Q,D=R,E=S,K=Y,L=Z,M=A1,0>=G+1] f33(A,B,C,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],95]: 1+it1*(3+it2*(2)+it3*(2)) Such that:it1=<-1*G,it1=<-1*G+1 it3=<-1*G+1*F,it2=<-1*G+1*F with precondition: [F=1,N=1,0>=G+1] f33(A,B,C,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],96]: 1+it1*(2)+it2*(3+it3*(2)+it4*(2)) Such that:it1+it2=<-1*G,it1+it2=<-1*G+1,it2=<-1*G,it2=<-1*G+1 it4=<-1*G+1*F,it3=<-1*G+1*F with precondition: [F=1,N=1,0>=G+2] f33(A,B,C,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],97]: 1+it1*(3+it2*(2)+it3*(2)) Such that:it1=<-1*G,it1=<1*F+ -1*G,it1=<1*T+ -1*G it3=<-1*G+1*F,it2=<-1*G+1*F with precondition: [N=0,U=1,X=0,A=O,B=P,C=Q,D=R,E=S,F=T,F+1=V,K=Y,L=Z,M=A1,0>=F,F>=G+1] f33(A,B,C,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],97]: 1+it1*(3+it2*(2+it3*(1))+it4*(2+it5*(1))) Such that:it1=<1*F+ -1*G,it1=<1*T+ -1,it1=<1*V+ -2,it1=<1*X+ -1,it1=<1*X+ -1*G it4=<1*F+ -1,it4=<-1*G+1*F,it2=<1*F+ -1,it2=<-1*G+1*F it3=<1*F+ -1 it5=<1*F with precondition: [N=0,U=1,A=O,B=P,C=Q,D=R,E=S,F=T,F+1=V,F=X,K=Y,L=Z,M=A1,G>=1,F>=G+1] f33(A,B,C,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,[94],97]: 4+it1*(3+it2*(2+it3*(1))+it4*(2+it5*(1)))+it6*(1)+it7*(2+it8*(1)) Such that:it1=<1*F+ -1,it1=<1*T+ -1,it1=<1*V+ -2,it1=<1*X+ -1,it6=<1*F,it6=<1*T,it6=<1*X,it6=<1*V+ -1,it7=<1*F,it7=<1*T,it7=<1*X,it7=<1*V+ -1 it4=<1*F+ -1,it2=<1*F+ -1 it3=<1*F+ -1 it5=<1*F it8=<1 with precondition: [G=0,N=0,U=1,A=O,B=P,C=Q,D=R,E=S,F=T,F+1=V,F=X,K=Y,L=Z,M=A1,F>=2] f33(A,B,C,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,97]: 4+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1,it2=<1 it3=<1 with precondition: [F=1,G=0,N=0,T=1,U=1,V=2,X=1,A=O,B=P,C=Q,D=R,E=S,K=Y,L=Z,M=A1] Inferred cost of f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f70(A,B,C,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]: 1 with precondition: [H=0,N=0,V=0,O=A,P=B,Q=C,R=D,S=E,W=I,X=J,Y=K,Z=L,A1=M,F=T,G+1=U,0>=G,F>=G] f70(A,B,C,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],100]: 1+it1*(1) Such that:it1=<1*F,it1=<1*G,it1=<1*T,it1=<1*V,it1=<1*F+ -1*H,it1=<1*T+ -1*H,it1=<1*U+ -1,it1=<1*V+ -1*H with precondition: [N=0,U=G+1,A=O,B=P,C=Q,D=R,E=S,F=T,U=V+1,J=X,K=Y,L=Z,M=A1,H>=0,U>=H+2,F+1>=U] Inferred cost of f66(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f66(A,B,C,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: [N=0,O=A,P=B,Q=C,R=D,S=E,V=H,W=I,X=J,Y=K,Z=L,A1=M,F=T,F=U+1,G>=F+1] f66(A,B,C,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],[103],104]: 1+it1*(2+it2*(1))+it3*(2) Such that:it1=<1*F,it1=<1*T,it1=<1*V,it1=<1*U+1,it3=<-1*G+1,it3=<1*V+ -1*G+1 it2=<1*F with precondition: [N=0,U+1=F,A=O,B=P,C=Q,D=R,E=S,U+1=T,U+1=V,J=X,K=Y,L=Z,M=A1,0>=G,U>=0] f66(A,B,C,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],104]: 1+it1*(2) Such that:it1=<-1*G+1,it1=<1*F+ -1*G+1,it1=<1*T+ -1*G+1 with precondition: [N=0,V=0,A=O,B=P,C=Q,D=R,E=S,F=T,F=U+1,J=X,K=Y,L=Z,M=A1,0>=F,F>=G] f66(A,B,C,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],104]: 1+it1*(2+it2*(1)) Such that:it1=<1*T,it1=<1*V,it1=<1*U+1,it1=<1*F+ -1*G+1,it1=<1*V+ -1*G+1 it2=<1*F with precondition: [N=0,U+1=F,A=O,B=P,C=Q,D=R,E=S,U+1=T,U+1=V,J=X,K=Y,L=Z,M=A1,G>=1,U+1>=G] Inferred cost of f84(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f84(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[107]: 1 with precondition: [N=0,O=A,P=B,Q=C,R=D,S=E,G+1=H,W=I,X=J,Y=K,Z=L,A1=M,F=T,G=U+1,G+1=V,G>=0,G>=F] f84(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[106],107]: 1+it1*(1) Such that:it1=<-1*G+1*T,it1=<1*V+ -1,it1=<-1*U+1*T+ -1,it1=<-1*U+1*V+ -2,it1=<1*F+ -1*H+1,it1=<1*T+ -1*H+1 with precondition: [N=0,V=F+1,A=O,B=P,C=Q,D=R,E=S,V=T+1,G=U+1,J=X,K=Y,L=Z,M=A1,G>=0,H>=G+1,V>=H+1] Inferred cost of f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[111]: 1 with precondition: [N=1,Y=0,Z=0,O=A,P=B,Q=C,R=D,S=E,T=F,V=H,W=I,X=J,A1=M,G=U,0>=G+1] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[109],[110],111]: 1+it1*(2+it2*(1))+it3*(2) Such that:it1=<1*F,it1=<1*G,it1=<1*T,it1=<1*V+ -1,it3=<1*G+1,it3=<1*G+ -1*F+1,it3=<1*G+ -1*T+1 it2=<1*G,it2=<1*F with precondition: [N=1,U+1=0,Y=0,Z=0,A=O,B=P,C=Q,D=R,E=S,F=T,F+1=V,J=X,M=A1,F>=1,G>=F] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[109],111]: 1+it1*(2) Such that:it1=<1*G+1,it1=<1*G+ -1*F+1,it1=<1*G+ -1*T+1 with precondition: [N=1,U+1=0,V=1,Y=0,Z=0,A=O,B=P,C=Q,D=R,E=S,F=T,J=X,M=A1,0>=F,G>=0] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[110],111]: 1+it1*(2+it2*(1)) Such that:it1=<1*F,it1=<1*T,it1=<1*G+1,it1=<1*V+ -1 it2=<1*F with precondition: [N=1,U+1=0,Y=0,Z=0,A=O,B=P,C=Q,D=R,E=S,F=T,F+1=V,J=X,M=A1,G>=0,F>=G+1] Inferred cost of loop_cont_f66(A,B,C,D,E,F,G,H,I,J,K,L,M): loop_cont_f66(A,B,C,D,E,F,G,H,I,J,K,L,M):[113]: 1 with precondition: [0>=G+1] loop_cont_f66(A,B,C,D,E,F,G,H,I,J,K,L,M):[114]: 1+it1*(2+it2*(1))+it3*(2) Such that:it1=<1*F,it1=<1*G,it3=<1*G,it3=<1*G+1,it3=<1*G+ -1*F+1 it2=<1*G,it2=<1*F with precondition: [F>=1,G>=F] loop_cont_f66(A,B,C,D,E,F,G,H,I,J,K,L,M):[115]: 1+it1*(2) Such that:it1=<1*G+1,it1=<1*G+ -1*F+1 with precondition: [0>=F,G>=0] loop_cont_f66(A,B,C,D,E,F,G,H,I,J,K,L,M):[116]: 1+it1*(2+it2*(1)) Such that:it1=<1*F,it1=<1*G+1 it2=<1*F with precondition: [G>=0,F>=G+1] Inferred cost of loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M): loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M):[118]: 2 with precondition: [0>=F,G>=F+1] loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M):[119]: 2+it1*(2+it2*(1)) Such that:it1=<1*F,it1=<1*G+ -1 it2=<1*G+ -1,it2=<1*F with precondition: [F>=1,G>=F+1] loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M):[120]: 2+it1*(2+it2*(1))+it3*(2)+it4*(2+it5*(1)) Such that:it1=<1*F,it3=<-1*G+1,it3=<1*F+ -1*G+1,it4=<1*F it2=<1*F it5=<1*F with precondition: [0>=G,F>=1] loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M):[121]: 2+it1*(2) Such that:it1=<-1*G+1,it1=<1*F+ -1*G+1 with precondition: [0>=F,F>=G] loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M):[122]: 2+it1*(2+it2*(1))+it3*(2+it4*(1)) Such that:it1=<1*F,it1=<1*F+ -1*G+1,it3=<1*F it2=<1*F it4=<1*F with precondition: [G>=1,F>=G] Inferred cost of loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M): loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[124]: 3 with precondition: [0>=F,G>=F] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[125]: 3+it1*(2+it2*(1))+it3*(2+it4*(1)) Such that:it1=<1*F,it1=<1*G,it3=<1*F,it3=<1*G it2=<1*G,it2=<1*F it4=<1*G,it4=<1*F with precondition: [F>=1,G>=F] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[126]: 6+it1*(3+it2*(2+it3*(1))+it4*(2+it5*(1)))+it6*(1)+it7*(2+it8*(1))+it9*(3+it10*(2)+it11*(2))+it12*(2+it13*(1))+it14*(2+it15*(1)) Such that:it1=<1*F+ -1,it6=<1*F,it7=<1*F,it9=<-1*G,it9=<1*F+ -1*G,it12=<1*F,it14=<1*F it4=<1*F+ -1,it2=<1*F+ -1 it3=<1*F+ -1 it5=<1*F it8=<1 it11=<1*F+ -1*G,it10=<1*F+ -1*G it13=<1*F it15=<1*F with precondition: [0>=G+1,F>=2] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[127]: 6+it1*(1)+it2*(2+it3*(1))+it4*(3+it5*(2)+it6*(2))+it7*(2+it8*(1))+it9*(2+it10*(1)) Such that:it1=<1,it2=<1,it4=<-1*G,it4=<-1*G+1,it7=<1,it9=<1 it3=<1 it6=<-1*G+1,it5=<-1*G+1 it8=<1 it10=<1 with precondition: [F=1,0>=G+1] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[128]: 3+it1*(3+it2*(2)+it3*(2)) Such that:it1=<-1*G,it1=<1*F+ -1*G it3=<1*F+ -1*G,it3=<-1*G,it2=<1*F+ -1*G,it2=<-1*G with precondition: [0>=F,F>=G+1] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[129]: 3+it1*(3+it2*(2+it3*(1))+it4*(2+it5*(1)))+it6*(2+it7*(1))+it8*(2+it9*(1)) Such that:it1=<1*F+ -1,it1=<1*F+ -1*G,it6=<1*F,it8=<1*F it4=<1*F+ -1*G,it4=<1*F+ -1,it2=<1*F+ -1*G,it2=<1*F+ -1 it3=<1*F+ -1 it5=<1*F it7=<1*F it9=<1*F with precondition: [G>=1,F>=G+1] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[130]: 6+it1*(3+it2*(2+it3*(1))+it4*(2+it5*(1)))+it6*(1)+it7*(2+it8*(1))+it9*(2+it10*(1))+it11*(2+it12*(1)) Such that:it1=<1*F+ -1,it6=<1*F,it7=<1*F,it9=<1*F,it11=<1*F it4=<1*F+ -1,it2=<1*F+ -1 it3=<1*F+ -1 it5=<1*F it8=<1 it10=<1*F it12=<1*F with precondition: [G=0,F>=2] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[131]: 6+it1*(1)+it2*(2+it3*(1))+it4*(2+it5*(1))+it6*(2+it7*(1)) Such that:it1=<1,it2=<1,it4=<1,it6=<1 it3=<1 it5=<1 it7=<1 with precondition: [F=1,G=0] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[132]: 1 with precondition: [F=1,0>=G] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[133]: 1+it1*(2) Such that:it1=<-1*G,it1=<-1*G+1 with precondition: [F=1,0>=G+1] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[134]: 1+it1*(3+it2*(2)+it3*(2)) Such that:it1=<-1*G,it1=<-1*G+1 it3=<-1*G+1,it2=<-1*G+1 with precondition: [F=1,0>=G+1] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[135]: 1+it1*(2)+it2*(3+it3*(2)+it4*(2)) Such that:it1+it2=<-1*G,it1+it2=<-1*G+1,it2=<-1*G,it2=<-1*G+1 it4=<-1*G+1,it3=<-1*G+1 with precondition: [F=1,0>=G+2] Inferred cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M): f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[137]: 14+it1*(1)+it2*(3+it3*(1))+it4*(1)+it5*(1)+it6*(3+it7*(2+it8*(1))+it9*(2+it10*(1)))+it11*(1)+it12*(2+it13*(1))+it14*(2+it15*(1))+it16*(2+it17*(1)) Such that:it1=<5,it2=<4,it4=<19,it5=<5,it6=<4,it11=<5,it12=<5,it14=<5,it16=<5 it3=<5,it3=<4 it9=<4,it7=<4 it8=<4 it10=<5 it13=<1 it15=<5 it17=<5 with precondition: [] Solved cost expressions of f0(A,B,C,D,E,F,G,H,I,J,K,L,M): f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[137]: 381 with precondition: [] Maximum cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M): 381 Asymptotic class: constant Time statistics: Partial evaluation computed in 166 ms. Invariants computed in 973 ms. ----Backward Invariants 437 ms. ----Transitive Invariants 135 ms. Refinement performed in 839 ms. Termination proved in 309 ms. Upper bounds computed in 1675 ms. ----Phase cost structures 790 ms. --------Equation cost structures 685 ms. --------Inductive compression(1) 33 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 852 ms. ----Solving cost expressions 1 ms. Compressed phase information: 26 Compressed Chains: 0 Compressed invariants: 1 Total analysis performed in 4286 ms.