warning: Ignored call to evalfstop/6 in equation evalfreturnin/6 
Inferred cost of evalfbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M): 
evalfbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M):[21]: 1
  with precondition: [G=0,H=A,I=B,C=E,D=F+1,C=J,D=K,C=L,D=M+1,D>=C+1] 

Inferred cost of evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M): 
evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M):[24]: 2
  with precondition: [G=0,B=C+1,L=E,M=F,A=H,B=I,B=J+1,A+B=D+1,A+B=K+1,A>=1,B>=2] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M):[25]: 1
  with precondition: [G=0,B=C+1,L=E,M=F,A=H,B=I,B=J+1,A+B=D+1,A+B=K+1,0>=A,B>=2] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[23],24]: 2+it1*(5)
  Such that:it1=<1/2*A,it1=<1/2*H,it1=<1/2*D+ -1/2*C,it1=<1/2*D+ -1/2*L,it1=<-1/2*M+1/2*A+1/2*B,it1=<-1/2*M+1/2*B+1/2*H,it1=<-1/2*M+1/2*H+1/2*I,it1=<1/2*D+ -1/2*B+1/2,it1=<1/2*D+ -1/2*M+1/2,it1=<-1/2*M+1/2*C+1/2*H+1/2
  with precondition: [G=0,B=C+1,A=H,B=I,B=J+1,B=L+1,K+1=M,B>=2,K>=B,D>=K+2,A+B>=D+1] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[23],25]: 1+it1*(5)
  Such that:it1=<1/2*A,it1=<1/2*H,it1=<1/2*D+ -1/2*C,it1=<1/2*D+ -1/2*K,it1=<1/2*D+ -1/2*L,it1=<-1/2*K+1/2*C+1/2*H,it1=<1/2*D+ -1/2*B+1/2,it1=<-1/2*K+1/2*A+1/2*B+ -1/2,it1=<-1/2*K+1/2*B+1/2*H+ -1/2,it1=<-1/2*K+1/2*H+1/2*I+ -1/2
  with precondition: [G=0,B=C+1,A=H,B=I,B=J+1,B=L+1,K+1=M,B>=2,K+2>=B,B>=K+1,D>=K+2,A+B>=D+1] 

Inferred cost of evalfbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M): 
evalfbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M):[31]: 1
  with precondition: [G=0,A=B,J=C,K=D,L=E,M=F,A=H,A=I,1>=A] 

evalfbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[27,28,29,30],31]: 1+it1*(5)+it2*(4)+it3*(5)
  Such that:it1+it2=<1/2*B+ -1/2,it1+it2=<1/2*B+1/2*H+ -1/2*K,it3=<1/2*A+1/4*B+1/4,it3=<1/2*A+1/4*B+ -1/2*H+1/4,it3=<1/2*A+1/4*B+ -1/4*I+1/2,it3=<1/2*A+1/4*B+ -1/4*H+ -1/4*K+1/2
  with precondition: [G=0,J=I+1,H+J=K+1,2>=J,J>=1,B>=J+1,B+J+2*A>=2*K+1] 

Inferred cost of evalfreturnin(A,B,C,D,E,F): 
evalfreturnin(A,B,C,D,E,F):[33]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalfbb9in(A,B,C,D,E,F): 
loop_cont_evalfbb9in(A,B,C,D,E,F):[35]: 1
  with precondition: [] 

Inferred cost of evalfentryin(A,B,C,D,E,F): 
evalfentryin(A,B,C,D,E,F):[37]: 3
  with precondition: [1>=B] 

evalfentryin(A,B,C,D,E,F):[38]: 3+it1*(5)+it2*(4)+it3*(5)
  Such that:it1+it2=<1/2*B,it1+it2=<1/2*B+ -1/2,it3=<3/4*B+1/2,it3=<3/4*B+1/4
  with precondition: [B>=2] 

Inferred cost of evalfstart(A,B,C,D,E,F): 
evalfstart(A,B,C,D,E,F):[40]: 4
  with precondition: [1>=B] 

evalfstart(A,B,C,D,E,F):[41]: 4+it1*(5)+it2*(4)+it3*(5)
  Such that:it1+it2=<1/2*B,it1+it2=<1/2*B+ -1/2,it3=<3/4*B+1/2,it3=<3/4*B+1/4
  with precondition: [B>=2] 

Solved cost expressions of evalfstart(A,B,C,D,E,F): 
evalfstart(A,B,C,D,E,F):[40]: 4  with precondition: [1>=B] 
evalfstart(A,B,C,D,E,F):[41]: 25/4*B+11/4  with precondition: [B>=2] 
Maximum cost of evalfstart(A,B,C,D,E,F): max([25/4*B+11/4,4]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 32 ms.
Invariants computed in 60 ms.
----Backward Invariants 30 ms.
----Transitive Invariants 9 ms.
Refinement performed in 55 ms.
Termination proved in 22 ms.
Upper bounds computed in 111 ms.
----Phase cost structures 60 ms.
--------Equation cost structures 50 ms.
--------Inductive compression(1) 10 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 45 ms.
----Solving cost expressions 2 ms.

Compressed phase information: 1 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 323 ms.