warning: Ignored call to loop_cont_f96/7 in equation loop_cont_f86/7 Inferred cost of f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[37]: 0 with precondition: [A=5,B=18,C=0,D=0,H=1,I=5,J=18,K=0,L=0,M=E,N=F,O=G] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[33,[35],36]: 2+it1*(1) Such that:it1=<4 with precondition: [A=5,B=18,C=0,D=0,H=0,I=5,J=18,K=0,L=0,E=M,F=N,G=O] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[33,[35],37]: 1+it1*(1) Such that:it1=<3,it1=<4,it1=<1*L+ -1 with precondition: [A=5,B=18,C=0,D=0,H=1,I=5,J=18,K=0,E=M,F=N,G=O,4>=L,L>=2] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[33,37]: 1 with precondition: [A=5,B=18,C=0,D=0,H=1,I=5,J=18,K=0,L=1,E=M,F=N,G=O] Inferred cost of f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[40]: 1 with precondition: [E=0,H=0,M=0,K=C,N=F,O=G,A=I,B=J,D+1=L,0>=B,A>=D+1] f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[39],40]: 1+it1*(1) Such that:it1=<1*J,it1=<1*M,it1=<1*B+ -1*E,it1=<1*J+ -1*E with precondition: [H=0,M=B,A=I,M=J,C=K,D+1=L,E>=0,A>=D+1,M>=E+1] Inferred cost of f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[44]: 1 with precondition: [H=0,L=0,J=B,K=C,M=E,N=F,O=G,A=I,D>=A] f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[42],44]: 1+it1*(2) Such that:it1=<1*A+ -1*D,it1=<1*I+ -1*D with precondition: [H=0,L=0,M=0,A=I,B=J,C=K,F=N,G=O,0>=B,A>=D+1] f72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[43],44]: 1+it1*(2+it2*(1)) Such that:it1=<1*A+ -1*D,it1=<1*I+ -1*D it2=<1*B with precondition: [H=0,L=0,A=I,B=J,C=K,B=M,B>=1,A>=D+1] Inferred cost of f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[47]: 1 with precondition: [H=0,L=0,I=A,K=C,M=E,N=F,O=G,B=J,D>=B] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[48]: 1 with precondition: [H=1,I=A,K=C,M=E,B=J,D=L,B>=D+1] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[46],47]: 1+it1*(1) Such that:it1=<1*B+ -1*D,it1=<1*J+ -1*D with precondition: [H=0,L=0,A=I,B=J,C=K,E=M,B>=D+1] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[46],48]: 1+it1*(1) Such that:it1=<1*B+ -1*D,it1=<1*J+ -1*D,it1=<1*L+ -1*D with precondition: [H=1,A=I,B=J,C=K,E=M,L>=D+1,B>=L+1] Inferred cost of f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[51]: 1 with precondition: [H=1,J=B,K=C,M=E,N=F,O=G,A=I,D=L,D>=A] f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[50],51]: 1+it1*(1) Such that:it1=<1*A+ -1*D,it1=<1*I+ -1*D with precondition: [H=1,A=I,B=J,C=K,A=L,E=M,F=N,G=O,A>=D+1] Inferred cost of loop_cont_f86(A,B,C,D,E,F,G): loop_cont_f86(A,B,C,D,E,F,G):[53]: 1 with precondition: [D>=A] loop_cont_f86(A,B,C,D,E,F,G):[54]: 1+it1*(1) Such that:it1=<1*A+ -1*D with precondition: [A>=D+1] Inferred cost of loop_cont_f72(A,B,C,D,E,F,G): loop_cont_f72(A,B,C,D,E,F,G):[56]: 2 with precondition: [0>=A,D>=B] loop_cont_f72(A,B,C,D,E,F,G):[57]: 2+it1*(1) Such that:it1=<1*A with precondition: [A>=1,D>=B] loop_cont_f72(A,B,C,D,E,F,G):[58]: 2+it1*(1) Such that:it1=<1*B+ -1*D with precondition: [0>=A,B>=D+1] loop_cont_f72(A,B,C,D,E,F,G):[59]: 2+it1*(1)+it2*(1) Such that:it1=<1*B+ -1*D,it2=<1*A with precondition: [A>=1,B>=D+1] loop_cont_f72(A,B,C,D,E,F,G):[60]: 1 with precondition: [B>=D+1] loop_cont_f72(A,B,C,D,E,F,G):[61]: 1+it1*(1) Such that:it1=<1*B+ -1*D,it1=<-1*D+1*B+ -1 with precondition: [B>=D+2] Inferred cost of loop_cont_f64(A,B,C,D,E,F,G): loop_cont_f64(A,B,C,D,E,F,G):[63]: 3 with precondition: [0>=A,0>=B,D>=A] loop_cont_f64(A,B,C,D,E,F,G):[64]: 3+it1*(1) Such that:it1=<1*A,it1=<1*D with precondition: [0>=B,A>=1,D>=A] loop_cont_f64(A,B,C,D,E,F,G):[65]: 3+it1*(1) Such that:it1=<1*B with precondition: [0>=A,B>=1,D>=A] loop_cont_f64(A,B,C,D,E,F,G):[66]: 3+it1*(1)+it2*(1) Such that:it1=<1*B,it2=<1*A,it2=<1*D with precondition: [A>=1,B>=1,D>=A] loop_cont_f64(A,B,C,D,E,F,G):[67]: 2 with precondition: [B>=1,D>=A] loop_cont_f64(A,B,C,D,E,F,G):[68]: 2+it1*(1) Such that:it1=<1*B,it1=<1*B+ -1 with precondition: [B>=2,D>=A] loop_cont_f64(A,B,C,D,E,F,G):[69]: 3+it1*(2) Such that:it1=<-1*D,it1=<1*A+ -1*D with precondition: [0>=A,0>=B,A>=D+1] loop_cont_f64(A,B,C,D,E,F,G):[70]: 3+it1*(2)+it2*(1) Such that:it1=<1*A+ -1*D,it2=<1*A with precondition: [0>=B,A>=1,A>=D+1] loop_cont_f64(A,B,C,D,E,F,G):[71]: 3+it1*(2+it2*(1))+it3*(1) Such that:it1=<-1*D,it1=<1*A+ -1*D,it3=<1*B it2=<1*B with precondition: [0>=A,B>=1,A>=D+1] loop_cont_f64(A,B,C,D,E,F,G):[72]: 3+it1*(2+it2*(1))+it3*(1)+it4*(1) Such that:it1=<1*A+ -1*D,it3=<1*B,it4=<1*A it2=<1*B with precondition: [A>=1,B>=1,A>=D+1] loop_cont_f64(A,B,C,D,E,F,G):[73]: 2+it1*(2+it2*(1)) Such that:it1=<1*A+ -1*D it2=<1*B with precondition: [B>=1,A>=D+1] loop_cont_f64(A,B,C,D,E,F,G):[74]: 2+it1*(2+it2*(1))+it3*(1) Such that:it1=<1*A+ -1*D,it3=<1*B,it3=<1*B+ -1 it2=<1*B with precondition: [B>=2,A>=D+1] Inferred cost of f0(A,B,C,D,E,F,G): f0(A,B,C,D,E,F,G):[76]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1)+it5*(1) Such that:it1=<4,it2=<5,it4=<18,it5=<5 it3=<18 with precondition: [] f0(A,B,C,D,E,F,G):[77]: 5+it1*(1)+it2*(2+it3*(1)) Such that:it1=<4,it2=<5 it3=<18 with precondition: [] f0(A,B,C,D,E,F,G):[78]: 5+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<4,it2=<5,it4=<17,it4=<18 it3=<18 with precondition: [] f0(A,B,C,D,E,F,G):[79]: 1 with precondition: [] f0(A,B,C,D,E,F,G):[80]: 2+it1*(1) Such that:it1=<3,it1=<4 with precondition: [] f0(A,B,C,D,E,F,G):[81]: 2 with precondition: [] Solved cost expressions of f0(A,B,C,D,E,F,G): f0(A,B,C,D,E,F,G):[76]: 133 with precondition: [] f0(A,B,C,D,E,F,G):[77]: 109 with precondition: [] f0(A,B,C,D,E,F,G):[78]: 126 with precondition: [] f0(A,B,C,D,E,F,G):[79]: 1 with precondition: [] f0(A,B,C,D,E,F,G):[80]: 5 with precondition: [] f0(A,B,C,D,E,F,G):[81]: 2 with precondition: [] Maximum cost of f0(A,B,C,D,E,F,G): 133 Asymptotic class: constant Time statistics: Partial evaluation computed in 28 ms. Invariants computed in 134 ms. ----Backward Invariants 63 ms. ----Transitive Invariants 18 ms. Refinement performed in 142 ms. Termination proved in 39 ms. Upper bounds computed in 157 ms. ----Phase cost structures 75 ms. --------Equation cost structures 69 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 71 ms. ----Solving cost expressions 1 ms. Compressed phase information: 5 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 570 ms.