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

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

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

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

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):[28]: 2
  with precondition: [G=0,E=C,B=D+1,E=H,B=I+1,E=J,B=K+1,E=L,F=M,F>=E] 

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

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

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

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

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

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[31,32,33,34,35,37,38,39,40,41,42,43,45,46],[36],47]: 1+it1*(4)+it2*(6)+it3*(6+it4*(3))+it5*(5+it6*(3))+it7*(5)+it8*(4+it9*(3))+it10*(6+it11*(3))+it12*(6+it13*(3)+it14*(3))+it15*(5+it16*(3)+it17*(3))+it18*(5+it19*(3))+it20*(5+it21*(3)+it22*(3))+it23*(4+it24*(3)+it25*(3))
  Such that:it1+it2+it3+it5+it7+it8+it10+it12+it15+it18+it20+it23=<1*B+1,it2+it3+it5+it7+it8+it10+it12+it15+it18+it20+it23=<1*B+1
            it4=<1*F+1,it4=<1*F
            it6=<1*F+1
            it14=<1*F+1,it14=<1*F
            it17=<1*F+1
            it22=<1*F+2,it22=<1*F+1
            it25=<1*F+2
  with precondition: [G=0,I+1=0,K+1=0,J=F+1,J=H,J=L,J=M+1,0>=J+1,B>=1,J>=A+1] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[31,32,33,34,35,37,38,39,40,41,42,43,45,46],44,[36],47]: inf
  with precondition: [G=0,H+1=0,I+1=0,J+1=0,K+1=0,L+1=0,M=F,0>=M+2,A>=0,B>=2] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[31,32,33,34,35,37,38,39,40,41,42,43,45,46],44,47]: inf
  with precondition: [G=0,H+1=0,I+1=0,J+1=0,K+1=0,L+1=0,M=F,0>=M+2,A>=0,B>=1] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[31,32,33,34,35,37,38,39,40,41,42,43,45,46],47]: 1+it1*(6)+it2*(6+it3*(3))+it4*(5+it5*(3))+it6*(5)+it7*(4+it8*(3))+it9*(6+it10*(3))+it11*(6+it12*(3)+it13*(3))+it14*(5+it15*(3)+it16*(3))+it17*(5+it18*(3))+it19*(5+it20*(3)+it21*(3))+it22*(4+it23*(3)+it24*(3))
  Such that:it1+it2+it4+it6+it7+it9+it11+it14+it17+it19+it22=<1*B+1
            it3=<1*F+1,it3=<1*F
            it5=<1*F+1
            it13=<1*F+1,it13=<1*F
            it16=<1*F+1
            it21=<1*F+2,it21=<1*F+1
            it24=<1*F+2
  with precondition: [G=0,I+1=0,K+1=0,H=L,F=M,B>=0,H>=J] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M):[44,[36],47]: 5+it1*(4)+it2*(3)
  Such that:it1=<1*B,it2=<1*A+1
  with precondition: [G=0,H+1=0,I+1=0,J+1=0,K+1=0,L+1=0,F=M,0>=F+2,A>=0,B>=1] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M):[44,47]: 5+it1*(3)
  Such that:it1=<1*A+1
  with precondition: [B=0,G=0,H+1=0,I+1=0,J+1=0,K+1=0,L+1=0,F=M,0>=F+2,A>=0] 

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

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

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

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

evalfentryin(A,B,C,D,E,F):[55]: 3+it1*(4)+it2*(6)+it3*(5)+it4*(6+it5*(3))+it6*(5+it7*(3))+it8*(4+it9*(3))
  Such that:it1+it2+it3+it4+it6+it8=<1*A+1,it2+it3+it4+it6+it8=<1*A+1
  with precondition: [0>=F+2,A>=1,F>=B] 

evalfentryin(A,B,C,D,E,F):[56]: inf
  with precondition: [0>=F+2,A>=2,B>=0] 

evalfentryin(A,B,C,D,E,F):[57]: inf
  with precondition: [0>=F+2,A>=1,B>=0] 

evalfentryin(A,B,C,D,E,F):[58]: 3+it1*(6)+it2*(6+it3*(3))+it4*(5+it5*(3))+it6*(5)+it7*(4+it8*(3))+it9*(6+it10*(3))+it11*(6+it12*(3)+it13*(3))+it14*(5+it15*(3)+it16*(3))+it17*(5+it18*(3))+it19*(5+it20*(3)+it21*(3))+it22*(4+it23*(3)+it24*(3))
  Such that:it1+it2+it4+it6+it7+it9+it11+it14+it17+it19+it22=<1*A+1
            it3=<1*F+1,it3=<1*F
            it5=<1*F+1
            it13=<1*F+1,it13=<1*F
            it16=<1*F+1
            it21=<1*F+2,it21=<1*F+1
            it24=<1*F+2
  with precondition: [A>=0] 

evalfentryin(A,B,C,D,E,F):[59]: 7+it1*(4)+it2*(3)
  Such that:it1=<1*A,it2=<1*B+1
  with precondition: [0>=F+2,A>=1,B>=0] 

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

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

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

evalfstart(A,B,C,D,E,F):[64]: 4+it1*(4)+it2*(6)+it3*(5)+it4*(6+it5*(3))+it6*(5+it7*(3))+it8*(4+it9*(3))
  Such that:it1+it2+it3+it4+it6+it8=<1*A+1,it2+it3+it4+it6+it8=<1*A+1
  with precondition: [0>=F+2,A>=1,F>=B] 

evalfstart(A,B,C,D,E,F):[65]: inf
  with precondition: [0>=F+2,A>=2,B>=0] 

evalfstart(A,B,C,D,E,F):[66]: inf
  with precondition: [0>=F+2,A>=1,B>=0] 

evalfstart(A,B,C,D,E,F):[67]: 4+it1*(6)+it2*(6+it3*(3))+it4*(5+it5*(3))+it6*(5)+it7*(4+it8*(3))+it9*(6+it10*(3))+it11*(6+it12*(3)+it13*(3))+it14*(5+it15*(3)+it16*(3))+it17*(5+it18*(3))+it19*(5+it20*(3)+it21*(3))+it22*(4+it23*(3)+it24*(3))
  Such that:it1+it2+it4+it6+it7+it9+it11+it14+it17+it19+it22=<1*A+1
            it3=<1*F+1,it3=<1*F
            it5=<1*F+1
            it13=<1*F+1,it13=<1*F
            it16=<1*F+1
            it21=<1*F+2,it21=<1*F+1
            it24=<1*F+2
  with precondition: [A>=0] 

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

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

Solved cost expressions of evalfstart(A,B,C,D,E,F): 
evalfstart(A,B,C,D,E,F):[62]: 4  with precondition: [0>=A+1] 
evalfstart(A,B,C,D,E,F):[63]: 4*A+8  with precondition: [0>=B+1,A>=0,B>=F+1] 
evalfstart(A,B,C,D,E,F):[64]: inf  with precondition: [0>=F+2,A>=1,F>=B] 
evalfstart(A,B,C,D,E,F):[65]: inf  with precondition: [0>=F+2,A>=2,B>=0] 
evalfstart(A,B,C,D,E,F):[66]: inf  with precondition: [0>=F+2,A>=1,B>=0] 
evalfstart(A,B,C,D,E,F):[67]: inf  with precondition: [A>=0] 
evalfstart(A,B,C,D,E,F):[68]: 4*A+3*B+11  with precondition: [0>=F+2,A>=1,B>=0] 
evalfstart(A,B,C,D,E,F):[69]: 3*B+11  with precondition: [A=0,0>=F+2,B>=0] 
Maximum cost of evalfstart(A,B,C,D,E,F): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 33 ms.
Invariants computed in 256 ms.
----Backward Invariants 150 ms.
----Transitive Invariants 21 ms.
Refinement performed in 218 ms.
Termination proved in 93 ms.
Upper bounds computed in 652 ms.
----Phase cost structures 517 ms.
--------Equation cost structures 475 ms.
--------Inductive compression(1) 10 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 122 ms.
----Solving cost expressions 5 ms.

Compressed phase information: 14 
Compressed Chains: 0 
Compressed invariants: 2 
Total analysis performed in 1300 ms.