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

evalfbb3in(A,B,C,D,E,F,G,H,I,J,K):[23]: 1
  with precondition: [F=0,D=C,K=E,A=G,B=H,D=I,D=J,A>=0,D>=0,D>=B+1] 

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

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

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

evalfbb7in(A,B,C,D,E,F,G,H,I,J,K):[31]: 0
  with precondition: [C=0,F=1,I=0,A=B,J=D,K=E,A=G,A=H,A>=0] 

evalfbb7in(A,B,C,D,E,F,G,H,I,J,K):[33]: 0
  with precondition: [C=0,F=1,I=0,A=B,J=D,K=E,A=G,A=H] 

evalfbb7in(A,B,C,D,E,F,G,H,I,J,K):[[25,26,27,28,29],30]: 1+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<1*C+1+nat(min([1*A+1,1*B+1,1*H+1]))*max([min([1*B,1*H]),min([1*B+1,1*H+1])]),it2+it3+it5=<1*A+1,it2+it3+it5=<1*B+1,it2+it3+it5=<1*H+1,it4=<2*B+1,it4=<2*H+1,it4=<-1*C+2*H+1,it4=<1*H+1*I+2,it4=<-1*C+1*B+1*I+2,it4=<-1*C+1*H+1*I+2,it4=<1*A+1*H+ -1*C+1,it4=<1*A+1*I+ -1*C+2
            it6=<1*B+1
  with precondition: [F=0,G+1=0,J+1=0,H=B,I+1=K,A>=0,C>=0,I+1>=0,H>=A] 

evalfbb7in(A,B,C,D,E,F,G,H,I,J,K):[[25,26,27,28,29],31]: 0+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<1*C+1+nat(min([1*A+1,1*B+1,1*H+1]))*max([min([1*B,1*H]),min([1*B+1,1*H+1])]),it2+it3+it5=<-1*J+1*B,it2+it3+it5=<-1*J+1*H,it2+it3+it5=<1*A+1,it2+it3+it5=<1*A+ -1*J,it2+it3+it5=<1*B+1,it2+it3+it5=<1*H+1,it4=<-1*G+2*H,it4=<-1*J+2*B,it4=<-1*J+2*H,it4=<2*B+1,it4=<2*H+1,it4=<-1*C+ -1*G+2*H,it4=<-1*C+2*H+1,it4=<1*H+1*I+2,it4=<-1*C+ -1*J+1*B+1*K,it4=<-1*C+1*B+1*I+2,it4=<-1*C+1*H+1*I+2,it4=<-1*J+1*H+1*I+1,it4=<1*A+1*H+ -1*C+1,it4=<1*A+1*H+ -1*C+ -1*G,it4=<1*A+1*I+ -1*C+2,it4=<1*A+1*K+ -1*C+ -1*J,it4=<-1*C+ -1*J+1*H+1*I+1
            it6=<1*B+1
  with precondition: [F=1,H=B,G=J,I+1=K,C>=0,G>=0,I+1>=0,H>=A,A>=G] 

evalfbb7in(A,B,C,D,E,F,G,H,I,J,K):[[25,26,27,28,29],32]: 1+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<1*C+1+nat(min([1*A+1,1*B+1,1*H+1]))*max([min([1*B,1*H]),min([1*B+1,1*H+1])]),it2+it3+it5=<-1*J+1*B,it2+it3+it5=<-1*J+1*H,it2+it3+it5=<1*A+1,it2+it3+it5=<1*A+ -1*J,it2+it3+it5=<1*B+1,it2+it3+it5=<1*H+1,it4=<-1*G+2*B,it4=<-1*J+1*H,it4=<-1*J+2*H,it4=<1*H+1,it4=<2*B+1,it4=<2*H+1,it4=<-1*C+ -1*J+1*B,it4=<-1*C+ -1*J+1*H,it4=<-1*C+ -1*J+2*H,it4=<-1*C+1*B+1,it4=<-1*C+1*H+1,it4=<-1*C+2*H+1,it4=<1*A+ -1*C+1,it4=<1*A+ -1*C+ -1*J,it4=<1*A+1*H+ -1*C+1,it4=<1*A+1*H+ -1*C+ -1*J
            it6=<1*B+1
  with precondition: [F=0,I+1=0,K=0,J=G,B=H,A>=0,C>=0,J+1>=0,B>=A,A>=J] 

evalfbb7in(A,B,C,D,E,F,G,H,I,J,K):[[25,26,27,28,29],33]: 0+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<1*C+1+nat(min([1*A+1,1*B+1,1*H+1]))*max([min([1*B,1*H]),min([1*B+1,1*H+1])]),it2+it3+it5=<-1*J+1*B,it2+it3+it5=<-1*J+1*H,it2+it3+it5=<1*A+1,it2+it3+it5=<1*A+ -1*J,it2+it3+it5=<1*B+1,it2+it3+it5=<1*H+1,it4=<-1*G+2*B,it4=<-1*J+2*H,it4=<2*B+1,it4=<2*H+1,it4=<-1*C+ -1*J+2*H,it4=<-1*C+2*H+1,it4=<-1*G+1*H+1*K,it4=<1*H+1*K+1,it4=<-1*C+ -1*G+1*H+1*K,it4=<-1*C+ -1*J+1*B+1*K,it4=<-1*C+1*B+1*K+1,it4=<-1*C+1*H+1*K+1,it4=<-1*J+1*H+1*I+1,it4=<1*A+1*H+ -1*C+1,it4=<1*A+1*H+ -1*C+ -1*J,it4=<1*A+1*K+ -1*C+1,it4=<1*A+1*K+ -1*C+ -1*G
            it6=<1*B+1
  with precondition: [F=1,H=B,G=J,I+1=K,A>=0,C>=0,G+1>=0,I>=0,H>=A,A>=G,A+C>=G+1] 

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

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

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

evalfentryin(A,B,C,D,E):[40]: 3+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B+1,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

evalfentryin(A,B,C,D,E):[41]: 3+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B+1,it4=<1*B+1,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

evalfentryin(A,B,C,D,E):[42]: 1
  with precondition: [B>=0] 

evalfentryin(A,B,C,D,E):[43]: 1
  with precondition: [] 

evalfentryin(A,B,C,D,E):[44]: 1+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B,it2+it3+it5=<1*B+1,it4=<2*B,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

evalfentryin(A,B,C,D,E):[45]: 1+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B+1,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

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

evalfstart(A,B,C,D,E):[48]: 4+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B+1,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

evalfstart(A,B,C,D,E):[49]: 4+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B+1,it4=<1*B+1,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

evalfstart(A,B,C,D,E):[50]: 2
  with precondition: [B>=0] 

evalfstart(A,B,C,D,E):[51]: 2
  with precondition: [] 

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

evalfstart(A,B,C,D,E):[53]: 2+it1*(3)+it2*(5)+it3*(6)+it4*(3)+it5*(5+it6*(3))
  Such that:it1+it2=<nat(min([1*B+1,1*B+1,1*B+1]))*max([min([1*B,1*B]),min([1*B+1,1*B+1])])+1,it2+it3+it5=<1*B+1,it4=<2*B+1
            it6=<1*B+1
  with precondition: [B>=0] 

Solved cost expressions of evalfstart(A,B,C,D,E): 
evalfstart(A,B,C,D,E):[47]: 4  with precondition: [0>=B+1] 
evalfstart(A,B,C,D,E):[48]: 6*B+3+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B+6, (3*B+8)* (1*B+1)]), (3*B+8)* (1*B+1)+nat((1*B+1)* (1*B+1)+1)*3,5*B+5+nat((1*B+1)* (1*B+1)+1)*3,6*B+6+nat((1*B+1)* (1*B+1)+1)*3])+4  with precondition: [B>=0] 
evalfstart(A,B,C,D,E):[49]: 3*B+3+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B+6, (3*B+8)* (1*B+1)]), (3*B+8)* (1*B+1)+nat((1*B+1)* (1*B+1)+1)*3,5*B+5+nat((1*B+1)* (1*B+1)+1)*3,6*B+6+nat((1*B+1)* (1*B+1)+1)*3])+4  with precondition: [B>=0] 
evalfstart(A,B,C,D,E):[50]: 2  with precondition: [B>=0] 
evalfstart(A,B,C,D,E):[51]: 2  with precondition: [] 
evalfstart(A,B,C,D,E):[52]: 6*B+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B, (3*B+8)* (1*B)]),nat((1*B+1)* (1*B+1)+1)*3+5*B,nat((1*B+1)* (1*B+1)+1)*3+6*B, (3*B+8)* (1*B)+nat((1*B+1)* (1*B+1)+1)*3])+2  with precondition: [B>=0] 
evalfstart(A,B,C,D,E):[53]: 6*B+3+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B+6, (3*B+8)* (1*B+1)]), (3*B+8)* (1*B+1)+nat((1*B+1)* (1*B+1)+1)*3,5*B+5+nat((1*B+1)* (1*B+1)+1)*3,6*B+6+nat((1*B+1)* (1*B+1)+1)*3])+2  with precondition: [B>=0] 
Maximum cost of evalfstart(A,B,C,D,E): max([4,6*B+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B, (3*B+8)* (1*B)]),nat((1*B+1)* (1*B+1)+1)*3+5*B,nat((1*B+1)* (1*B+1)+1)*3+6*B, (3*B+8)* (1*B)+nat((1*B+1)* (1*B+1)+1)*3])+2,3*B+3+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B+6, (3*B+8)* (1*B+1)]), (3*B+8)* (1*B+1)+nat((1*B+1)* (1*B+1)+1)*3,5*B+5+nat((1*B+1)* (1*B+1)+1)*3,6*B+6+nat((1*B+1)* (1*B+1)+1)*3])+4,6*B+3+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B+6, (3*B+8)* (1*B+1)]), (3*B+8)* (1*B+1)+nat((1*B+1)* (1*B+1)+1)*3,5*B+5+nat((1*B+1)* (1*B+1)+1)*3,6*B+6+nat((1*B+1)* (1*B+1)+1)*3])+2,6*B+3+max([nat((1*B+1)* (1*B+1)+1)*3+max([6*B+6, (3*B+8)* (1*B+1)]), (3*B+8)* (1*B+1)+nat((1*B+1)* (1*B+1)+1)*3,5*B+5+nat((1*B+1)* (1*B+1)+1)*3,6*B+6+nat((1*B+1)* (1*B+1)+1)*3])+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 23 ms.
Invariants computed in 106 ms.
----Backward Invariants 73 ms.
----Transitive Invariants 8 ms.
Refinement performed in 59 ms.
Termination proved in 19 ms.
Upper bounds computed in 272 ms.
----Phase cost structures 141 ms.
--------Equation cost structures 117 ms.
--------Inductive compression(1) 13 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 116 ms.
----Solving cost expressions 7 ms.

Compressed phase information: 4 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 518 ms.