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,B=H,C=I,D=J,0>=D,B+C>=D] 

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

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

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

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*G,it1=<1*I+ -1,it1=<1*J+ -2,it1=<1*K+ -2,it1=<-1*B+1*J+ -1,it1=<-1*H+1*J+ -1,it1=<1*A+ -1*C+1,it1=<1*G+ -1*C+1
            it2=<1*A+1*B,it2=<1*A+1
            it3=<1*B+2*A,it3=<1*A+1*B
  with precondition: [F=0,A=G,B=H,A+1=I,A+B+1=J,A+B+1=K,B>=1,C>=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):[40]: 1
  with precondition: [F=0,G=A,I=C,J=D,K=E,B=H,0>=B] 

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

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

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

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

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

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

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

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

evalfstart(A,B,C,D,E):[51]: 4+it1*(3)
  Such that:it1=<1*A
  with precondition: [0>=B,A>=1] 

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

Solved cost expressions of evalfstart(A,B,C,D,E): 
evalfstart(A,B,C,D,E):[50]: 4  with precondition: [0>=A] 
evalfstart(A,B,C,D,E):[51]: 3*A+4  with precondition: [0>=B,A>=1] 
evalfstart(A,B,C,D,E):[52]: 1*A*nat(1*B*nat((2*A+2*B+3)* (1*B+1)+3)+3)+4  with precondition: [A>=1,B>=1] 
Maximum cost of evalfstart(A,B,C,D,E): max([3*A+4,4,1*A*nat(1*B*nat((2*A+2*B+3)* (1*B+1)+3)+3)+4]) 
Asymptotic class: n^4 
Time statistics: 
Partial evaluation computed in 26 ms.
Invariants computed in 113 ms.
----Backward Invariants 46 ms.
----Transitive Invariants 21 ms.
Refinement performed in 77 ms.
Termination proved in 45 ms.
Upper bounds computed in 533 ms.
----Phase cost structures 194 ms.
--------Equation cost structures 141 ms.
--------Inductive compression(1) 7 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 331 ms.
----Solving cost expressions 2 ms.

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