warning: Ignored call to evalfstop/5 in equation evalfreturnin/5 
Inferred cost of evalfbb4in(A,B,C,D,E,F,G,H,I,J,K): 
evalfbb4in(A,B,C,D,E,F,G,H,I,J,K):[26]: 1
  with precondition: [E=1,F=0,K=1,G=A,I=C,B=H,D=J,0>=D,B>=D] 

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

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

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K):[[28],[29],30]: 1+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1*B,it1=<1*H,it1=<1*J+ -1,it1=<1*K+ -1,it3=<-1*A,it3=<-1*C,it3=<-1*G,it3=<-1*I,it3=<-1*D+1,it3=<-1*G+1*B,it3=<1*K+ -1*D,it3=<-1*A+1*K+ -1,it3=<-1*C+1*J+ -1,it3=<-1*G+1*K+ -1,it3=<-1*I+1*J+ -1
            it2=<-1*C+1*B+ -1,it2=<-1*A+1*B+ -1,it2=<1*B
  with precondition: [F=0,H=B,I=C,A=G,H+1=J,H+1=K,0>=D,H>=1,D>=A+1,A>=I] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K):[[28],30]: 1+it1*(3)
  Such that:it1=<-1*A,it1=<-1*C,it1=<-1*G,it1=<-1*I,it1=<-1*D+1,it1=<-1*G+1*B,it1=<-1*I+1*H,it1=<1*J+ -1*D,it1=<-1*A+1*J+ -1,it1=<-1*C+1*J+ -1,it1=<-1*G+1*J+ -1,it1=<-1*I+1*J+ -1
  with precondition: [F=0,K=1,J=B+1,I=C,A=G,J=H+1,1>=J,D>=A+1,J>=D+1,A>=I] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K):[[29],30]: 1+it1*(3+it2*(2))
  Such that:it1=<1*B,it1=<-1*G+1*B,it1=<1*K+ -1,it1=<1*K+ -1*D,it1=<-1*A+1*K+ -1,it1=<-1*C+1*K+ -1,it1=<-1*G+1*K+ -1
            it2=<1*B
  with precondition: [F=0,H=B,A=G,C=I,H+1=J,H+1=K,D>=1,D>=A+1,A>=C,H>=D] 

Inferred cost of evalfbb8in(A,B,C,D,E,F,G,H,I,J,K): 
evalfbb8in(A,B,C,D,E,F,G,H,I,J,K):[36]: 1
  with precondition: [C=1,F=0,I=1,J=D,K=E,A+1=G,B=H,0>=A,B>=A] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K):[[32],36]: 1+it1*(3)
  Such that:it1=<1*H,it1=<1*G+ -1,it1=<1*G+ -1*C,it1=<1*I+ -1,it1=<1*J+ -1,it1=<1*A+ -1*C+1,it1=<1*B+ -1*C+1
  with precondition: [F=0,A=B,A+1=G,A=H,A+1=I,A+1=J,E=K,C>=1,A>=C] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K):[[35],36]: 1+it1*(3+it2*(3+it3*(2)))
  Such that:it1=<1*B+ -1,it1=<1*G+ -1,it1=<1*G+ -1*C,it1=<1*H+ -1,it1=<1*I+ -1,it1=<1*J+ -2,it1=<1*K+ -2,it1=<1*A+ -1*C+1,it1=<1*J+ -1*C+ -1
            it2=<1*B+ -1*A,it2=<1*B+ -1,it2=<-1*C+1*B,it2=<1*B
            it3=<1*B
  with precondition: [F=0,A+1=G,B=H,A+1=I,B+1=J,B+1=K,C>=1,B>=A+1,A>=C] 

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

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K):[[40],39,41]: 3+it1*(3)+it2*(2+it3*(3+it4*(3+it5*(2))))
  Such that:it1=<1*B,it1=<1*H,it1=<1*G+ -1,it1=<1*I+ -1,it1=<1*J+ -1,it1=<1*K+ -1,it2=<1*B+ -1,it2=<1*G+ -2,it2=<1*H+ -1,it2=<1*H+ -1*A,it2=<1*I+ -2,it2=<1*J+ -2,it2=<1*K+ -2
            it3=<1*B+ -1
            it4=<1*B+ -1,it4=<-1*A+1*B,it4=<1*B
            it5=<1*B
  with precondition: [F=0,G=B+1,G=H+1,G=I,G=J,G=K,A>=1,G>=A+2] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K):[39,41]: 3+it1*(3)
  Such that:it1=<1
  with precondition: [A=1,B=1,F=0,G=2,H=1,I=2,J=2,E=K] 

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

Inferred cost of loop_cont_evalfbb10in(A,B,C,D,E): 
loop_cont_evalfbb10in(A,B,C,D,E):[45]: 1
  with precondition: [] 

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

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

evalfentryin(A,B,C,D,E):[49]: 5+it1*(3)
  Such that:it1=<1
  with precondition: [B=1] 

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

evalfstart(A,B,C,D,E):[52]: 6+it1*(3)+it2*(2+it3*(3+it4*(3+it5*(2))))
  Such that:it1=<1*B,it2=<1*B+ -1
            it3=<1*B+ -1
            it4=<1*B+ -1,it4=<1*B
            it5=<1*B
  with precondition: [B>=2] 

evalfstart(A,B,C,D,E):[53]: 6+it1*(3)
  Such that:it1=<1
  with precondition: [B=1] 

Solved cost expressions of evalfstart(A,B,C,D,E): 
evalfstart(A,B,C,D,E):[51]: 4  with precondition: [0>=B] 
evalfstart(A,B,C,D,E):[52]: (1*B+ -1)*nat((1*B+ -1)*nat((2*B+3)* (1*B+ -1)+3)+2)+3*B+6  with precondition: [B>=2] 
evalfstart(A,B,C,D,E):[53]: 9  with precondition: [B=1] 
Maximum cost of evalfstart(A,B,C,D,E): max([9, (1*B+ -1)*nat((1*B+ -1)*nat((2*B+3)* (1*B+ -1)+3)+2)+3*B+6]) 
Asymptotic class: n^4 
Time statistics: 
Partial evaluation computed in 24 ms.
Invariants computed in 124 ms.
----Backward Invariants 51 ms.
----Transitive Invariants 21 ms.
Refinement performed in 85 ms.
Termination proved in 45 ms.
Upper bounds computed in 579 ms.
----Phase cost structures 189 ms.
--------Equation cost structures 154 ms.
--------Inductive compression(1) 4 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 380 ms.
----Solving cost expressions 1 ms.

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