warning: Ignored call to loop_cont_f83/10 in equation loop_cont_f75/10 Inferred cost of f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[50]: 1 with precondition: [A=0,D=0,K=0,L=0,O=0,M=B,N=C,R=G,S=H,T=I,U=J,E=P,E=Q+1,0>=E] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[49],50]: 1+it1*(1) Such that:it1=<1*E,it1=<1*O,it1=<1*P,it1=<1*P+ -1*D,it1=<1*Q+1 with precondition: [A=0,K=0,L=0,Q+1=E,B=M,C=N,Q+1=O,Q+1=P,G=R,H=S,I=T,J=U,D>=0,Q>=D] Inferred cost of f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[53]: 1 with precondition: [K=0,R=0,L=A,M=B,N=C,O=D,P=E,S=H,T=I,U=J,F=Q,0>=F+1] f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[52],53]: 1+it1*(1) Such that:it1=<1*F+1 with precondition: [K=0,Q+1=0,R=0,A=L,B=M,C=N,D=O,E=P,H=S,I=T,J=U,F>=0] Inferred cost of f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[56]: 1 with precondition: [K=0,L=0,M=B,N=C,O=D,Q=F,S=H,T=I,U=J,E=P,G=R,G>=E] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[55],56]: 1+it1*(1) Such that:it1=<1*E+ -1*G,it1=<1*P+ -1*G with precondition: [K=0,L=0,B=M,C=N,D=O,E=P,F=Q,E=R,H=S,I=T,J=U,E>=G+1] Inferred cost of f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[59]: 1 with precondition: [K=0,S=0,M=B,N=C,O=D,Q=F,R=G,T=I,U=J,A=L,E=P,A>=E] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[58],59]: 1+it1*(1) Such that:it1=<1*L+ -1*A,it1=<1*P+ -1*A with precondition: [K=0,S=0,E=L,B=M,C=N,D=O,E=P,F=Q,G=R,I=T,J=U,E>=A+1] Inferred cost of f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[62]: 1 with precondition: [K=0,L=A,M=B,N=C,O=D,Q=F,R=G,U=J,E=P,H=S,E=T+1,H>=E] f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[61],62]: 1+it1*(1) Such that:it1=<1*E+ -1*H,it1=<1*S+ -1*H with precondition: [K=0,A=L,B=M,C=N,D=O,E=P,F=Q,G=R,E=S,E=T+1,J=U,E>=H+1] Inferred cost of f65(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f65(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[65]: 1 with precondition: [K=0,U=0,L=A,M=B,N=C,O=D,P=E,Q=F,R=G,S=H,I=T,0>=I+1] f65(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[64],65]: 1+it1*(1) Such that:it1=<1*I+1 with precondition: [K=0,T+1=0,U=0,A=L,B=M,C=N,D=O,E=P,F=Q,G=R,H=S,I>=0] Inferred cost of f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[68]: 1 with precondition: [K=0,M=B,N=C,O=D,Q=F,R=G,S=H,T=I,E=L+1,E=P,J=U,J>=E] f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[67],68]: 1+it1*(1) Such that:it1=<1*E+ -1*J,it1=<1*P+ -1*J with precondition: [K=0,E=L+1,B=M,C=N,D=O,E=P,F=Q,G=R,H=S,I=T,E=U,E>=J+1] Inferred cost of f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[71]: 1 with precondition: [K=1,M=B,N=C,O=D,P=E,Q=F,R=G,S=H,T=I,U=J,A=L,0>=A+1] f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[70],71]: 1+it1*(1) Such that:it1=<1*A+1 with precondition: [K=1,L+1=0,B=M,C=N,D=O,E=P,F=Q,G=R,H=S,I=T,J=U,A>=0] Inferred cost of loop_cont_f75(A,B,C,D,E,F,G,H,I,J): loop_cont_f75(A,B,C,D,E,F,G,H,I,J):[73]: 1 with precondition: [0>=A+1] loop_cont_f75(A,B,C,D,E,F,G,H,I,J):[74]: 1+it1*(1) Such that:it1=<1*A+1 with precondition: [A>=0] Inferred cost of loop_cont_f65(A,B,C,D,E,F,G,H,I,J): loop_cont_f65(A,B,C,D,E,F,G,H,I,J):[76]: 2 with precondition: [0>=E,J>=E] loop_cont_f65(A,B,C,D,E,F,G,H,I,J):[77]: 2+it1*(1) Such that:it1=<1*E,it1=<1*J with precondition: [E>=1,J>=E] loop_cont_f65(A,B,C,D,E,F,G,H,I,J):[78]: 2+it1*(1) Such that:it1=<-1*J,it1=<1*E+ -1*J with precondition: [0>=E,E>=J+1] loop_cont_f65(A,B,C,D,E,F,G,H,I,J):[79]: 2+it1*(1)+it2*(1) Such that:it1=<1*E+ -1*J,it2=<1*E with precondition: [E>=1,E>=J+1] Inferred cost of loop_cont_f55(A,B,C,D,E,F,G,H,I,J): loop_cont_f55(A,B,C,D,E,F,G,H,I,J):[81]: 3 with precondition: [0>=E,0>=I+1] loop_cont_f55(A,B,C,D,E,F,G,H,I,J):[82]: 3+it1*(1)+it2*(1) Such that:it1=<1*E,it2=<1*E with precondition: [0>=I+1,E>=1] loop_cont_f55(A,B,C,D,E,F,G,H,I,J):[83]: 3+it1*(1) Such that:it1=<1*I+1 with precondition: [0>=E,I>=0] loop_cont_f55(A,B,C,D,E,F,G,H,I,J):[84]: 3+it1*(1)+it2*(1)+it3*(1) Such that:it1=<1*I+1,it2=<1*E,it3=<1*E with precondition: [E>=1,I>=0] Inferred cost of loop_cont_f45(A,B,C,D,E,F,G,H,I,J): loop_cont_f45(A,B,C,D,E,F,G,H,I,J):[86]: 4 with precondition: [0>=E,H>=E] loop_cont_f45(A,B,C,D,E,F,G,H,I,J):[87]: 4+it1*(1)+it2*(1)+it3*(1) Such that:it1=<1*E,it1=<1*H,it2=<1*E,it2=<1*H,it3=<1*E,it3=<1*H with precondition: [E>=1,H>=E] loop_cont_f45(A,B,C,D,E,F,G,H,I,J):[88]: 4+it1*(1) Such that:it1=<-1*H,it1=<1*E+ -1*H with precondition: [0>=E,E>=H+1] loop_cont_f45(A,B,C,D,E,F,G,H,I,J):[89]: 4+it1*(1)+it2*(1)+it3*(1)+it4*(1) Such that:it1=<1*E+ -1*H,it2=<1*E,it3=<1*E,it4=<1*E with precondition: [E>=1,E>=H+1] Inferred cost of loop_cont_f37(A,B,C,D,E,F,G,H,I,J): loop_cont_f37(A,B,C,D,E,F,G,H,I,J):[91]: 5 with precondition: [0>=E,A>=E] loop_cont_f37(A,B,C,D,E,F,G,H,I,J):[92]: 5+it1*(1)+it2*(1)+it3*(1)+it4*(1) Such that:it1=<1*A,it1=<1*E,it2=<1*A,it2=<1*E,it3=<1*A,it3=<1*E,it4=<1*A,it4=<1*E with precondition: [E>=1,A>=E] loop_cont_f37(A,B,C,D,E,F,G,H,I,J):[93]: 5+it1*(1) Such that:it1=<1*E+ -1*A with precondition: [0>=E,E>=A+1] loop_cont_f37(A,B,C,D,E,F,G,H,I,J):[94]: 5+it1*(1)+it2*(1)+it3*(1)+it4*(1)+it5*(1) Such that:it1=<1*E+ -1*A,it2=<1*E,it3=<1*E,it4=<1*E,it5=<1*E with precondition: [E>=1,E>=A+1] Inferred cost of loop_cont_f27(A,B,C,D,E,F,G,H,I,J): loop_cont_f27(A,B,C,D,E,F,G,H,I,J):[96]: 6 with precondition: [0>=E,G>=E] loop_cont_f27(A,B,C,D,E,F,G,H,I,J):[97]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)+it5*(1) Such that:it1=<1*E,it1=<1*G,it2=<1*E,it2=<1*G,it3=<1*E,it3=<1*G,it4=<1*E,it4=<1*G,it5=<1*E,it5=<1*G with precondition: [E>=1,G>=E] loop_cont_f27(A,B,C,D,E,F,G,H,I,J):[98]: 6+it1*(1) Such that:it1=<-1*G,it1=<1*E+ -1*G with precondition: [0>=E,E>=G+1] loop_cont_f27(A,B,C,D,E,F,G,H,I,J):[99]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)+it5*(1)+it6*(1) Such that:it1=<1*E+ -1*G,it2=<1*E,it3=<1*E,it4=<1*E,it5=<1*E,it6=<1*E with precondition: [E>=1,E>=G+1] Inferred cost of loop_cont_f17(A,B,C,D,E,F,G,H,I,J): loop_cont_f17(A,B,C,D,E,F,G,H,I,J):[101]: 7 with precondition: [0>=E,0>=F+1] loop_cont_f17(A,B,C,D,E,F,G,H,I,J):[102]: 7+it1*(1)+it2*(1)+it3*(1)+it4*(1)+it5*(1)+it6*(1) Such that:it1=<1*E,it2=<1*E,it3=<1*E,it4=<1*E,it5=<1*E,it6=<1*E with precondition: [0>=F+1,E>=1] loop_cont_f17(A,B,C,D,E,F,G,H,I,J):[103]: 7+it1*(1) Such that:it1=<1*F+1 with precondition: [0>=E,F>=0] loop_cont_f17(A,B,C,D,E,F,G,H,I,J):[104]: 7+it1*(1)+it2*(1)+it3*(1)+it4*(1)+it5*(1)+it6*(1)+it7*(1) Such that:it1=<1*F+1,it2=<1*E,it3=<1*E,it4=<1*E,it5=<1*E,it6=<1*E,it7=<1*E with precondition: [E>=1,F>=0] Inferred cost of f0(A,B,C,D,E,F,G,H,I,J): f0(A,B,C,D,E,F,G,H,I,J):[106]: 9 with precondition: [0>=E] f0(A,B,C,D,E,F,G,H,I,J):[107]: 9+it1*(1)+it2*(1)+it3*(1)+it4*(1)+it5*(1)+it6*(1)+it7*(1)+it8*(1) Such that:it1=<1*E,it2=<1*E,it3=<1*E,it4=<1*E,it5=<1*E,it6=<1*E,it7=<1*E,it8=<1*E with precondition: [E>=1] Solved cost expressions of f0(A,B,C,D,E,F,G,H,I,J): f0(A,B,C,D,E,F,G,H,I,J):[106]: 9 with precondition: [0>=E] f0(A,B,C,D,E,F,G,H,I,J):[107]: 8*E+9 with precondition: [E>=1] Maximum cost of f0(A,B,C,D,E,F,G,H,I,J): max([8*E+9,9]) Asymptotic class: n Time statistics: Partial evaluation computed in 49 ms. Invariants computed in 181 ms. ----Backward Invariants 76 ms. ----Transitive Invariants 36 ms. Refinement performed in 221 ms. Termination proved in 85 ms. Upper bounds computed in 190 ms. ----Phase cost structures 103 ms. --------Equation cost structures 96 ms. --------Inductive compression(1) 1 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 72 ms. ----Solving cost expressions 2 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 846 ms.