warning: Ignored call to loop_cont_f18/7 in equation loop_cont_f8/7 Inferred cost of f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[23],24]: 1+it1*(1) Such that:it1=<100,it1=<-1*C+101 with precondition: [A+1=0,B+1=0,H=0,I+1=0,J+1=0,K=101,L=1,M=0,F=N,G=O,100>=C,C>=1] Inferred cost of f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[29]: 0 with precondition: [E=1,F=1,H=1,M=1,N=1,I=A,J=B,K=C,O=G,D=L,99>=D] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[31]: 0 with precondition: [E=1,F=1,H=1,M=1,N=1,I=A,J=B,K=C,O=G,D=L,99>=D] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[26,27],28]: 1+it1*(1) Such that:it1=<99,it1=<-1*D+100,it1=<-1*F+100,it1=<-1*L+100,it1=<1*E+98,it1=<98/97*M+99,it1=<-1*D+98/97*M+100,it1=<-1*F+ -1*L+101,it1=<-1*L+1*E+99,it1=<-1*L+98/97*M+100 with precondition: [H=0,N=100,A=I,B=J,C=K,D=L,1>=D,1>=E,99>=F,E+F>=2,E+9601>=98*M+96*F,98*M+9700>=97*E+97*F] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[26,27],29]: 0+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*F+100,it1=<-1*L+100,it1=<1*E+98,it1=<1*N+ -1,it1=<1*N+ -1*F,it1=<98/97*M+99,it1=<-1*D+98/97*M+100,it1=<-1*F+ -1*L+101,it1=<-1*L+1*E+99,it1=<-1*L+98/97*M+100,it1=<1*E+1*N+ -2,it1=<1*N+98/97*M+ -1 with precondition: [H=1,A=I,B=J,C=K,D=L,1>=E,99>=N,101>=D+N,N>=F+1,E+F>=2,E+95*N+1>=97*M+95*F,96*N+97*M>=96*E+96*F] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[26,27],30]: 1+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*F+100,it1=<-1*L+100,it1=<1*E+98,it1=<1*N+ -1,it1=<1*N+ -1*F,it1=<98/97*M+99,it1=<1*E+1*N+ -2,it1=<1*N+98/97*M+ -1 with precondition: [H=0,A=I,B=J,C=K,D=L,D+N=101,1>=E,D>=2,100>=D+F,E+F>=2,E+9596>=97*M+95*D+95*F,97*M+9696>=96*D+96*E+96*F] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[26,27],31]: 0+it1*(1) Such that:it1=<99,it1=<-1*D+100,it1=<-1*F+100,it1=<-1*L+100,it1=<1*E+98,it1=<1*N+ -1,it1=<1*N+ -1*F,it1=<98/97*M+99,it1=<-1*D+98/97*M+100,it1=<-1*F+ -1*L+101,it1=<-1*L+1*E+99,it1=<-1*L+98/97*M+100,it1=<1*E+1*N+ -2,it1=<1*N+98/97*M+ -1 with precondition: [H=1,A=I,B=J,C=K,D=L,1>=E,100>=N,101>=D+N,N>=F+1,E+F>=2,E+96*N+1>=98*M+96*F,97*N+98*M>=97*E+97*F] Inferred cost of f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[35]: 3+it1*(1) Such that:it1=<99,it1=<-1*D+100,it1=<-1*L+100,it1=<98/97*M+99,it1=<98/97*M+ -1*D+100,it1=<98/97*M+ -1*L+100,it1=<9505/97 with precondition: [H=1,N=100,I=A,J=B,K=C,D=L,1>=D,0>=M+1,M+97>=0] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[36]: 3+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*D+9602/97,it1=<-1*L+100,it1=<-1*L+9602/97,it1=<1*N+ -1,it1=<1*N+ -195/97,it1=<98/97*M+99,it1=<98/97*M+1*N+ -1,it1=<9408/97,it1=<9505/97 with precondition: [H=1,I=A,J=B,K=C,D=L,D+N=101,0>=M+1,D>=2,97*M+9504>=96*D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[37]: 3+it1*(1) Such that:it1=<99,it1=<197,it1=<-1*D+100,it1=<-1*L+100,it1=<98/97*M+99,it1=<98/97*M+ -1*D+100,it1=<98/97*M+ -1*L+100 with precondition: [H=1,N=100,I=A,J=B,K=C,D=L,1>=D,97>=M,M>=1] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[38]: 3+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*L+100,it1=<1*N+ -1,it1=<-18719/9409*D+1872096/9409,it1=<-18719/9409*L+1872096/9409,it1=<-9310/9409*D+1862687/9409,it1=<-9310/9409*L+1862687/9409,it1=<98/97*M+99,it1=<9310/9409*N+922377/9409,it1=<18719/9409*N+ -18523/9409,it1=<98/97*M+1*N+ -1,it1=<18914/97,it1=<19011/97 with precondition: [H=1,I=A,J=B,K=C,D=L,D+N=101,D>=2,M>=1,9502>=97*M+95*D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[39]: 1 with precondition: [H=1,99>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[40]: 1 with precondition: [H=1,99>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[41]: 1+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*D+19108/97,it1=<-18719/9409*D+1872096/9409,it1=<-9310/9409*D+1862687/9409,it1=<18914/97,it1=<19011/97 with precondition: [H=1,99>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[42]: 1+it1*(1) Such that:it1=<99,it1=<197,it1=<-1*D+100,it1=<-1*D+198,it1=<-193/97*D+19302/97,it1=<-96/97*D+19205/97 with precondition: [H=1,99>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[43]: 1 with precondition: [H=1,I=A,J=B,K=C,M=E,N=F,O=G,D=L,D>=100] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],36]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<97,it1=<98,it1=<99,it1=<-1*L+100,it1=<-1*L+9602/97,it1=<1*N+ -1,it1=<1*N+ -195/97,it1=<98/97*M+99,it1=<98/97*M+1*N+ -1,it1=<9311/97,it1=<9505/97,it2=<98,it2=<-1*N+99,it2=<1*L+ -2,it2=<97/96*M+97,it2=<9215/96,it3=<9701,it3=<9702,it3=<-98*N+9799,it3=<-97*N+9798,it3=<-97*N+9799,it3=<-1*N+9702,it3=<1*L+9601,it3=<97*L+1,it3=<97*L+2,it3=<98*L+ -99,it3=<97/96*M+9700,it3=<4753/48*M+9603,it3=<9409/96*M+9604,it3=<9409/96*M+9605,it3=<456191/48,it3=<912575/96,it3=<912671/96,it3=<931103/96,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [H=1,A=I,B=J,C=K,L+N=101,1>=D,0>=M+1,L>=3,97*M+9504>=96*L] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],38]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<97,it1=<98,it1=<99,it1=<-1*L+100,it1=<1*N+ -1,it1=<-18719/9409*L+1872096/9409,it1=<-9310/9409*L+1862687/9409,it1=<98/97*M+99,it1=<9310/9409*N+922377/9409,it1=<18719/9409*N+ -18523/9409,it1=<98/97*M+1*N+ -1,it1=<18914/97,it1=<19011/97,it1=<1815939/9409,it1=<1834757/9409,it2=<97,it2=<98,it2=<-1*N+99,it2=<1*L+ -2,it2=<-97/95*M+9312/95,it3=<9603,it3=<9604,it3=<9605,it3=<9700,it3=<9701,it3=<9702,it3=<-98*N+9799,it3=<-97*N+9798,it3=<-97*N+9799,it3=<-1*N+9702,it3=<1*L+9601,it3=<97*L+1,it3=<97*L+2,it3=<98*L+ -99,it3=<-9506/95*M+921791/95,it3=<-9409/95*M+921789/95,it3=<-9409/95*M+921884/95,it3=<-97/95*M+921597/95,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [H=1,A=I,B=J,C=K,L+N=101,1>=D,L>=3,M>=1,9502>=97*M+95*L] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],39]: 1+it1*(3)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<97,it1=<98,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it3=<-1*D+2 it4=<-1*D+100,it4=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],40]: 1+it1*(3)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<97,it1=<98,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it3=<-1*D+2 it4=<-1*D+100,it4=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],41]: 1+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1+it2=<98,it1+it2=<18914/97,it1+it2=<19110/97,it1+it2=<1825348/9409,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<940996/97,it1+it3=<941093/97,it1+it3=<941190/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950405/97,it1+it3=<950601/97,it1+it3=<92179975/9409,it2=<98,it3=<9701,it3=<9702,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],42]: 1+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<99,it1=<197,it1+it2=<98,it1+it2=<196,it1+it2=<18820/97,it1+it2=<19110/97,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<9702,it1+it3=<9703,it1+it3=<9704,it1+it3=<9799,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950311/97,it1+it3=<950601/97,it2=<98,it3=<9701,it3=<9702,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],[34],43]: 1+it1*(3)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<98,it2=<9701,it2=<9702,it3=<-1*D+2 it4=<-1*D+100,it4=<99 with precondition: [H=1,L=100,M=0,N=2,A=I,B=J,C=K,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],35]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<99,it1=<-1*D+99,it1=<-1*L+100,it1=<98/97*M+99,it1=<-1*D+98/97*M+99,it1=<98/97*M+ -1*L+100,it1=<9505/97,it2=<-1*D+2,it2=<1*L+ -1*D it3=<-1*D+100,it3=<99 with precondition: [H=1,N=100,A=I,B=J,C=K,1>=L,0>=M+1,M+97>=0,L>=D+1] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],36]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<98,it1=<99,it1=<98/97*M+98,it1=<98/97*M+99,it1=<9408/97,it1=<9505/97,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [H=1,L=2,N=99,A=I,B=J,C=K,1>=D,0>=M+1,M+96>=0] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],37]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<99,it1=<197,it1=<-1*D+99,it1=<-1*L+100,it1=<98/97*M+99,it1=<-1*D+98/97*M+99,it1=<98/97*M+ -1*L+100,it2=<-1*D+2,it2=<1*L+ -1*D it3=<-1*D+100,it3=<99 with precondition: [H=1,N=100,A=I,B=J,C=K,1>=L,97>=M,M>=1,L>=D+1] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],38]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<98,it1=<99,it1=<98/97*M+98,it1=<98/97*M+99,it1=<18914/97,it1=<19011/97,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [H=1,L=2,N=99,A=I,B=J,C=K,1>=D,96>=M,M>=1] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],39]: 1+it1*(3+it2*(1)) Such that:it1=<-1*D+2 it2=<-1*D+100,it2=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],40]: 1+it1*(3+it2*(1)) Such that:it1=<-1*D+2 it2=<-1*D+100,it2=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],41]: 1+it1*(1)+it2*(3+it3*(1)) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1+it2=<-1*D+100,it1+it2=<-1*D+19108/97,it1+it2=<-1*D+19205/97,it1+it2=<-18719/9409*D+1862786/9409,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],42]: 1+it1*(1)+it2*(3+it3*(1)) Such that:it1=<99,it1=<197,it1+it2=<-1*D+100,it1+it2=<-1*D+198,it1+it2=<-1*D+19207/97,it1+it2=<-193/97*D+198,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [H=1,1>=D] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],36]: 3+it1*(1)+it2*(3)+it3*(1) Such that:it1=<97,it1=<98,it1=<99,it1=<-1*D+99,it1=<-1*D+9505/97,it1=<-1*L+100,it1=<-1*L+9602/97,it1=<1*N+ -1,it1=<1*N+ -195/97,it1=<98/97*M+99,it1=<98/97*M+1*N+ -1,it1=<9311/97,it1=<9505/97,it2=<98,it2=<-1*D+100,it2=<-1*N+99,it2=<1*L+ -2,it2=<97/96*M+97,it2=<-1*D+ -1*N+101,it2=<9215/96,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-98*N+9799,it3=<-97*D+9896,it3=<-97*N+9798,it3=<-97*N+9799,it3=<-1*N+9702,it3=<1*L+9601,it3=<97*L+1,it3=<97*L+2,it3=<98*L+ -99,it3=<97/96*M+9700,it3=<4753/48*M+9603,it3=<9409/96*M+9604,it3=<9409/96*M+9605,it3=<-98*D+ -98*N+9995,it3=<-97*D+ -97*N+9993,it3=<-97*N+ -98*D+9994,it3=<-1*N+ -98*D+9898,it3=<456191/48,it3=<912575/96,it3=<912671/96,it3=<931103/96 with precondition: [H=1,A=I,B=J,C=K,L+N=101,0>=M+1,D>=2,97*M+9504>=96*L,L>=D+1] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],38]: 3+it1*(1)+it2*(3)+it3*(1) Such that:it1=<97,it1=<98,it1=<99,it1=<-1*D+99,it1=<-1*L+100,it1=<1*N+ -1,it1=<-18719/9409*D+1853377/9409,it1=<-18719/9409*L+1872096/9409,it1=<-9310/9409*D+1853377/9409,it1=<-9310/9409*L+1862687/9409,it1=<98/97*M+99,it1=<9310/9409*N+922377/9409,it1=<18719/9409*N+ -18523/9409,it1=<98/97*M+1*N+ -1,it1=<18914/97,it1=<19011/97,it1=<1815939/9409,it1=<1834757/9409,it2=<97,it2=<98,it2=<-1*D+100,it2=<-1*N+99,it2=<1*L+ -2,it2=<-97/95*M+9312/95,it2=<-1*D+ -1*N+101,it3=<9603,it3=<9604,it3=<9605,it3=<9700,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-98*N+9799,it3=<-97*D+9896,it3=<-97*N+9798,it3=<-97*N+9799,it3=<-1*N+9702,it3=<1*L+9601,it3=<97*L+1,it3=<97*L+2,it3=<98*L+ -99,it3=<-9506/95*M+921791/95,it3=<-9409/95*M+921789/95,it3=<-9409/95*M+921884/95,it3=<-97/95*M+921597/95,it3=<-98*D+ -98*N+9995,it3=<-97*D+ -97*N+9993,it3=<-97*N+ -98*D+9994,it3=<-1*N+ -98*D+9898 with precondition: [H=1,A=I,B=J,C=K,L+N=101,D>=2,M>=1,9502>=97*M+95*L,L>=D+1] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],39]: 1+it1*(3)+it2*(1) Such that:it1=<97,it1=<98,it1=<-1*D+99,it1=<-1*D+100,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it2=<-98*D+9799,it2=<-98*D+9800,it2=<-98*D+9896,it2=<-98*D+9897,it2=<-97*D+9799,it2=<-97*D+9896 with precondition: [H=1,98>=D,D>=2] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],40]: 1+it1*(3)+it2*(1) Such that:it1=<97,it1=<98,it1=<-1*D+99,it1=<-1*D+100,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it2=<-98*D+9799,it2=<-98*D+9800,it2=<-98*D+9896,it2=<-98*D+9897,it2=<-97*D+9799,it2=<-97*D+9896 with precondition: [H=1,98>=D,D>=2] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],41]: 1+it1*(1)+it2*(3)+it3*(1) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1+it2=<98,it1+it2=<-1*D+100,it1+it2=<-1*D+19108/97,it1+it2=<-1*D+19304/97,it1+it2=<-18719/9409*D+1862786/9409,it1+it2=<18914/97,it1+it2=<19110/97,it1+it2=<1825348/9409,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<-98*D+9800,it1+it3=<-98*D+9801,it1+it3=<-98*D+9897,it1+it3=<-98*D+950698/97,it1+it3=<-98*D+950795/97,it1+it3=<-98*D+960008/97,it1+it3=<-98*D+960105/97,it1+it3=<-98*D+960204/97,it1+it3=<-98*D+960301/97,it1+it3=<-98*D+969417/97,it1+it3=<-98*D+969613/97,it1+it3=<-97*D+9800,it1+it3=<-97*D+950698/97,it1+it3=<-97*D+960008/97,it1+it3=<-97*D+960204/97,it1+it3=<-931392/9409*D+94042759/9409,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<940996/97,it1+it3=<941093/97,it1+it3=<941190/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950405/97,it1+it3=<950601/97,it1+it3=<92179975/9409,it2=<98,it2=<-1*D+100,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-97*D+9896 with precondition: [H=1,98>=D,D>=2] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],42]: 1+it1*(1)+it2*(3)+it3*(1) Such that:it1=<99,it1=<197,it1+it2=<98,it1+it2=<196,it1+it2=<-1*D+100,it1+it2=<-1*D+198,it1+it2=<-1*D+19304/97,it1+it2=<-193/97*D+198,it1+it2=<18820/97,it1+it2=<19110/97,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<9702,it1+it3=<9703,it1+it3=<9704,it1+it3=<9799,it1+it3=<-98*D+9800,it1+it3=<-98*D+9801,it1+it3=<-98*D+9897,it1+it3=<-98*D+9898,it1+it3=<-98*D+9899,it1+it3=<-98*D+9995,it1+it3=<-98*D+950698/97,it1+it3=<-98*D+950795/97,it1+it3=<-98*D+960204/97,it1+it3=<-98*D+960301/97,it1+it3=<-98*D+969613/97,it1+it3=<-97*D+9800,it1+it3=<-97*D+9898,it1+it3=<-97*D+950698/97,it1+it3=<-97*D+960204/97,it1+it3=<-9602/97*D+9995,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950311/97,it1+it3=<950601/97,it2=<98,it2=<-1*D+100,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-97*D+9896 with precondition: [H=1,98>=D,D>=2] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],43]: 1+it1*(3)+it2*(1) Such that:it1=<98,it1=<-1*D+100,it2=<9701,it2=<9702,it2=<-98*D+9897,it2=<-97*D+9896 with precondition: [H=1,L=100,M=0,N=2,A=I,B=J,C=K,99>=D,D>=2] Inferred cost of loop_cont_f8(A,B,C,D,E,F,G): loop_cont_f8(A,B,C,D,E,F,G):[45]: 3+it1*(1) Such that:it1=<99,it1=<-1*D+100,it1=<-1*D+9602/97,it1=<9505/97 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[46]: 3+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*D+9602/97,it1=<9408/97,it1=<9505/97 with precondition: [9407>=96*D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[47]: 3+it1*(1) Such that:it1=<99,it1=<197,it1=<-1*D+100,it1=<-1*D+198 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[48]: 3+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-18719/9409*D+1872096/9409,it1=<-9310/9409*D+1862687/9409,it1=<18914/97,it1=<19011/97 with precondition: [99>=D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[49]: 1 with precondition: [99>=D] loop_cont_f8(A,B,C,D,E,F,G):[50]: 1 with precondition: [99>=D] loop_cont_f8(A,B,C,D,E,F,G):[51]: 1+it1*(1) Such that:it1=<98,it1=<99,it1=<-1*D+100,it1=<-1*D+19108/97,it1=<-18719/9409*D+1872096/9409,it1=<-9310/9409*D+1862687/9409,it1=<18914/97,it1=<19011/97 with precondition: [99>=D] loop_cont_f8(A,B,C,D,E,F,G):[52]: 1+it1*(1) Such that:it1=<99,it1=<197,it1=<-1*D+100,it1=<-1*D+198,it1=<-193/97*D+19302/97,it1=<-96/97*D+19205/97 with precondition: [99>=D] loop_cont_f8(A,B,C,D,E,F,G):[53]: 1 with precondition: [D>=100] loop_cont_f8(A,B,C,D,E,F,G):[54]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<97,it1=<98,it1=<99,it1=<9311/97,it1=<9505/97,it2=<98,it2=<9215/96,it3=<9701,it3=<9702,it3=<456191/48,it3=<912575/96,it3=<912671/96,it3=<931103/96,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[55]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<97,it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1=<1815939/9409,it1=<1834757/9409,it2=<97,it2=<98,it3=<9603,it3=<9604,it3=<9605,it3=<9700,it3=<9701,it3=<9702,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[56]: 1+it1*(3)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<97,it1=<98,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it3=<-1*D+2 it4=<-1*D+100,it4=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[57]: 1+it1*(3)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<97,it1=<98,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it3=<-1*D+2 it4=<-1*D+100,it4=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[58]: 1+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1+it2=<98,it1+it2=<18914/97,it1+it2=<19110/97,it1+it2=<1825348/9409,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<940996/97,it1+it3=<941093/97,it1+it3=<941190/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950405/97,it1+it3=<950601/97,it1+it3=<92179975/9409,it2=<98,it3=<9701,it3=<9702,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[59]: 1+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<99,it1=<197,it1+it2=<98,it1+it2=<196,it1+it2=<18820/97,it1+it2=<19110/97,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<9702,it1+it3=<9703,it1+it3=<9704,it1+it3=<9799,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950311/97,it1+it3=<950601/97,it2=<98,it3=<9701,it3=<9702,it4=<-1*D+2 it5=<-1*D+100,it5=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[60]: 1+it1*(3)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<98,it2=<9701,it2=<9702,it3=<-1*D+2 it4=<-1*D+100,it4=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[61]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<99,it1=<-1*D+99,it1=<-1*D+9505/97,it1=<9505/97,it2=<-1*D+1,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [0>=D] loop_cont_f8(A,B,C,D,E,F,G):[62]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<98,it1=<99,it1=<9408/97,it1=<9505/97,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[63]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<99,it1=<197,it1=<-1*D+99,it1=<-1*D+197,it2=<-1*D+1,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [0>=D] loop_cont_f8(A,B,C,D,E,F,G):[64]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[65]: 1+it1*(3+it2*(1)) Such that:it1=<-1*D+2 it2=<-1*D+100,it2=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[66]: 1+it1*(3+it2*(1)) Such that:it1=<-1*D+2 it2=<-1*D+100,it2=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[67]: 1+it1*(1)+it2*(3+it3*(1)) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1+it2=<-1*D+100,it1+it2=<-1*D+19108/97,it1+it2=<-1*D+19205/97,it1+it2=<-18719/9409*D+1862786/9409,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[68]: 1+it1*(1)+it2*(3+it3*(1)) Such that:it1=<99,it1=<197,it1+it2=<-1*D+100,it1+it2=<-1*D+198,it1+it2=<-1*D+19207/97,it1+it2=<-193/97*D+198,it2=<-1*D+2 it3=<-1*D+100,it3=<99 with precondition: [1>=D] loop_cont_f8(A,B,C,D,E,F,G):[69]: 3+it1*(1)+it2*(3)+it3*(1) Such that:it1=<97,it1=<98,it1=<99,it1=<-1*D+99,it1=<-1*D+9505/97,it1=<9311/97,it1=<9505/97,it2=<98,it2=<-1*D+100,it2=<-1*D+9407/96,it2=<9215/96,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-98*D+465599/48,it3=<-98*D+931391/96,it3=<-98*D+949919/96,it3=<-97*D+9896,it3=<-97*D+931295/96,it3=<456191/48,it3=<912575/96,it3=<912671/96,it3=<931103/96 with precondition: [9311>=96*D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[70]: 3+it1*(1)+it2*(3)+it3*(1) Such that:it1=<97,it1=<98,it1=<99,it1=<-1*D+99,it1=<-18719/9409*D+1853377/9409,it1=<-9310/9409*D+1853377/9409,it1=<18914/97,it1=<19011/97,it1=<1815939/9409,it1=<1834757/9409,it2=<97,it2=<98,it2=<-1*D+99,it2=<-1*D+100,it3=<9603,it3=<9604,it3=<9605,it3=<9700,it3=<9701,it3=<9702,it3=<-98*D+9799,it3=<-98*D+9800,it3=<-98*D+9896,it3=<-98*D+9897,it3=<-97*D+9799,it3=<-97*D+9896 with precondition: [98>=D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[71]: 1+it1*(3)+it2*(1) Such that:it1=<97,it1=<98,it1=<-1*D+99,it1=<-1*D+100,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it2=<-98*D+9799,it2=<-98*D+9800,it2=<-98*D+9896,it2=<-98*D+9897,it2=<-97*D+9799,it2=<-97*D+9896 with precondition: [98>=D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[72]: 1+it1*(3)+it2*(1) Such that:it1=<97,it1=<98,it1=<-1*D+99,it1=<-1*D+100,it2=<9603,it2=<9604,it2=<9605,it2=<9700,it2=<9701,it2=<9702,it2=<-98*D+9799,it2=<-98*D+9800,it2=<-98*D+9896,it2=<-98*D+9897,it2=<-97*D+9799,it2=<-97*D+9896 with precondition: [98>=D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[73]: 1+it1*(1)+it2*(3)+it3*(1) Such that:it1=<98,it1=<99,it1=<18914/97,it1=<19011/97,it1+it2=<98,it1+it2=<-1*D+100,it1+it2=<-1*D+19108/97,it1+it2=<-1*D+19304/97,it1+it2=<-18719/9409*D+1862786/9409,it1+it2=<18914/97,it1+it2=<19110/97,it1+it2=<1825348/9409,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<-98*D+9800,it1+it3=<-98*D+9801,it1+it3=<-98*D+9897,it1+it3=<-98*D+950698/97,it1+it3=<-98*D+950795/97,it1+it3=<-98*D+960008/97,it1+it3=<-98*D+960105/97,it1+it3=<-98*D+960204/97,it1+it3=<-98*D+960301/97,it1+it3=<-98*D+969417/97,it1+it3=<-98*D+969613/97,it1+it3=<-97*D+9800,it1+it3=<-97*D+950698/97,it1+it3=<-97*D+960008/97,it1+it3=<-97*D+960204/97,it1+it3=<-931392/9409*D+94042759/9409,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<940996/97,it1+it3=<941093/97,it1+it3=<941190/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950405/97,it1+it3=<950601/97,it1+it3=<92179975/9409,it2=<98,it2=<-1*D+100,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-97*D+9896 with precondition: [98>=D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[74]: 1+it1*(1)+it2*(3)+it3*(1) Such that:it1=<99,it1=<197,it1+it2=<98,it1+it2=<196,it1+it2=<-1*D+100,it1+it2=<-1*D+198,it1+it2=<-1*D+19304/97,it1+it2=<-193/97*D+198,it1+it2=<18820/97,it1+it2=<19110/97,it1+it3=<9604,it1+it3=<9605,it1+it3=<9606,it1+it3=<9701,it1+it3=<9702,it1+it3=<9703,it1+it3=<9704,it1+it3=<9799,it1+it3=<-98*D+9800,it1+it3=<-98*D+9801,it1+it3=<-98*D+9897,it1+it3=<-98*D+9898,it1+it3=<-98*D+9899,it1+it3=<-98*D+9995,it1+it3=<-98*D+950698/97,it1+it3=<-98*D+950795/97,it1+it3=<-98*D+960204/97,it1+it3=<-98*D+960301/97,it1+it3=<-98*D+969613/97,it1+it3=<-97*D+9800,it1+it3=<-97*D+9898,it1+it3=<-97*D+950698/97,it1+it3=<-97*D+960204/97,it1+it3=<-9602/97*D+9995,it1+it3=<931686/97,it1+it3=<931783/97,it1+it3=<931880/97,it1+it3=<941192/97,it1+it3=<941289/97,it1+it3=<941386/97,it1+it3=<950311/97,it1+it3=<950601/97,it2=<98,it2=<-1*D+100,it3=<9701,it3=<9702,it3=<-98*D+9897,it3=<-97*D+9896 with precondition: [98>=D,D>=2] loop_cont_f8(A,B,C,D,E,F,G):[75]: 1+it1*(3)+it2*(1) Such that:it1=<98,it1=<-1*D+100,it2=<9701,it2=<9702,it2=<-98*D+9897,it2=<-97*D+9896 with precondition: [99>=D,D>=2] Inferred cost of f0(A,B,C,D,E,F,G): f0(A,B,C,D,E,F,G):[77]: 5+it1*(1)+it2*(1) Such that:it1=<100,it2=<99,it2=<9505/97 with precondition: [] f0(A,B,C,D,E,F,G):[78]: 5+it1*(1)+it2*(1) Such that:it1=<100,it2=<99,it2=<197 with precondition: [] f0(A,B,C,D,E,F,G):[79]: 3+it1*(1) Such that:it1=<100 with precondition: [] f0(A,B,C,D,E,F,G):[80]: 3+it1*(1) Such that:it1=<100 with precondition: [] f0(A,B,C,D,E,F,G):[81]: 3+it1*(1)+it2*(1) Such that:it1=<100,it2=<98,it2=<99,it2=<18914/97,it2=<19011/97,it2=<1853377/9409 with precondition: [] f0(A,B,C,D,E,F,G):[82]: 3+it1*(1)+it2*(1) Such that:it1=<100,it2=<99,it2=<197 with precondition: [] f0(A,B,C,D,E,F,G):[83]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(1)+it5*(3+it6*(1)) Such that:it1=<100,it2=<97,it2=<98,it2=<99,it2=<9311/97,it2=<9505/97,it3=<98,it3=<9215/96,it4=<9701,it4=<9702,it4=<456191/48,it4=<912575/96,it4=<912671/96,it4=<931103/96,it5=<1 it6=<99 with precondition: [] f0(A,B,C,D,E,F,G):[84]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(1)+it5*(3+it6*(1)) Such that:it1=<100,it2=<97,it2=<98,it2=<99,it2=<18914/97,it2=<19011/97,it2=<1815939/9409,it2=<1834757/9409,it3=<97,it3=<98,it4=<9603,it4=<9604,it4=<9605,it4=<9700,it4=<9701,it4=<9702,it5=<1 it6=<99 with precondition: [] f0(A,B,C,D,E,F,G):[85]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<100,it2=<97,it2=<98,it3=<9603,it3=<9604,it3=<9605,it3=<9700,it3=<9701,it3=<9702,it4=<1 it5=<99 with precondition: [] f0(A,B,C,D,E,F,G):[86]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<100,it2=<97,it2=<98,it3=<9603,it3=<9604,it3=<9605,it3=<9700,it3=<9701,it3=<9702,it4=<1 it5=<99 with precondition: [] f0(A,B,C,D,E,F,G):[87]: 3+it1*(1)+it2*(1)+it3*(3)+it4*(1)+it5*(3+it6*(1)) Such that:it1=<100,it2=<98,it2=<99,it2=<18914/97,it2=<19011/97,it2+it3=<98,it2+it3=<18914/97,it2+it3=<19110/97,it2+it3=<1825348/9409,it2+it4=<9604,it2+it4=<9605,it2+it4=<9606,it2+it4=<9701,it2+it4=<931686/97,it2+it4=<931783/97,it2+it4=<931880/97,it2+it4=<940996/97,it2+it4=<941093/97,it2+it4=<941190/97,it2+it4=<941192/97,it2+it4=<941289/97,it2+it4=<941386/97,it2+it4=<950405/97,it2+it4=<950601/97,it2+it4=<92179975/9409,it3=<98,it4=<9701,it4=<9702,it5=<1 it6=<99 with precondition: [] f0(A,B,C,D,E,F,G):[88]: 3+it1*(1)+it2*(1)+it3*(3)+it4*(1)+it5*(3+it6*(1)) Such that:it1=<100,it2=<99,it2=<197,it2+it3=<98,it2+it3=<196,it2+it3=<18820/97,it2+it3=<19110/97,it2+it4=<9604,it2+it4=<9605,it2+it4=<9606,it2+it4=<9701,it2+it4=<9702,it2+it4=<9703,it2+it4=<9704,it2+it4=<9799,it2+it4=<931686/97,it2+it4=<931783/97,it2+it4=<931880/97,it2+it4=<941192/97,it2+it4=<941289/97,it2+it4=<941386/97,it2+it4=<950311/97,it2+it4=<950601/97,it3=<98,it4=<9701,it4=<9702,it5=<1 it6=<99 with precondition: [] f0(A,B,C,D,E,F,G):[89]: 3+it1*(1)+it2*(3)+it3*(1)+it4*(3+it5*(1)) Such that:it1=<100,it2=<98,it3=<9701,it3=<9702,it4=<1 it5=<99 with precondition: [] f0(A,B,C,D,E,F,G):[90]: 5+it1*(1)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<100,it2=<98,it2=<99,it2=<9408/97,it2=<9505/97,it3=<1 it4=<99 with precondition: [] f0(A,B,C,D,E,F,G):[91]: 5+it1*(1)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<100,it2=<98,it2=<99,it2=<18914/97,it2=<19011/97,it3=<1 it4=<99 with precondition: [] f0(A,B,C,D,E,F,G):[92]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<100,it2=<1 it3=<99 with precondition: [] f0(A,B,C,D,E,F,G):[93]: 3+it1*(1)+it2*(3+it3*(1)) Such that:it1=<100,it2=<1 it3=<99 with precondition: [] f0(A,B,C,D,E,F,G):[94]: 3+it1*(1)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<100,it2=<98,it2=<99,it2=<18914/97,it2=<19011/97,it2+it3=<99,it2+it3=<19011/97,it2+it3=<19108/97,it3=<1 it4=<99 with precondition: [] f0(A,B,C,D,E,F,G):[95]: 3+it1*(1)+it2*(1)+it3*(3+it4*(1)) Such that:it1=<100,it2=<99,it2=<197,it2+it3=<99,it2+it3=<197,it2+it3=<19013/97,it2+it3=<19110/97,it3=<1 it4=<99 with precondition: [] Solved cost expressions of f0(A,B,C,D,E,F,G): f0(A,B,C,D,E,F,G):[77]: 19690/97 with precondition: [] f0(A,B,C,D,E,F,G):[78]: 204 with precondition: [] f0(A,B,C,D,E,F,G):[79]: 103 with precondition: [] f0(A,B,C,D,E,F,G):[80]: 103 with precondition: [] f0(A,B,C,D,E,F,G):[81]: 201 with precondition: [] f0(A,B,C,D,E,F,G):[82]: 202 with precondition: [] f0(A,B,C,D,E,F,G):[83]: 94004059/9312 with precondition: [] f0(A,B,C,D,E,F,G):[84]: 10198 with precondition: [] f0(A,B,C,D,E,F,G):[85]: 10099 with precondition: [] f0(A,B,C,D,E,F,G):[86]: 10099 with precondition: [] f0(A,B,C,D,E,F,G):[87]: 10103 with precondition: [] f0(A,B,C,D,E,F,G):[88]: 10103 with precondition: [] f0(A,B,C,D,E,F,G):[89]: 10200 with precondition: [] f0(A,B,C,D,E,F,G):[90]: 29487/97 with precondition: [] f0(A,B,C,D,E,F,G):[91]: 305 with precondition: [] f0(A,B,C,D,E,F,G):[92]: 205 with precondition: [] f0(A,B,C,D,E,F,G):[93]: 205 with precondition: [] f0(A,B,C,D,E,F,G):[94]: 303 with precondition: [] f0(A,B,C,D,E,F,G):[95]: 10201 with precondition: [] Maximum cost of f0(A,B,C,D,E,F,G): 10201 Asymptotic class: constant Time statistics: Partial evaluation computed in 30 ms. Invariants computed in 262 ms. ----Backward Invariants 179 ms. ----Transitive Invariants 15 ms. Refinement performed in 166 ms. Termination proved in 32 ms. Upper bounds computed in 1874 ms. ----Phase cost structures 308 ms. --------Equation cost structures 288 ms. --------Inductive compression(1) 6 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 1537 ms. ----Solving cost expressions 6 ms. Compressed phase information: 44 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 2414 ms.