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

evalfbb1in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[20],21]: 1+it1*(1)
  Such that:it1=<-1*B+1*O,it1=<1*O+ -1*F
  with precondition: [H=0,C+1=E,N=G,A=I,N+1=J,C+1=K,D=L,C+1=M,N=O,F>=B,D>=C+1,N>=F+1] 

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

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

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

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

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

Inferred cost of loop_cont_evalfbb5in(A,B,C,D,E,F,G): 
loop_cont_evalfbb5in(A,B,C,D,E,F,G):[34]: 1
  with precondition: [] 

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

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

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

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

Solved cost expressions of evalfstart(A,B,C,D,E,F,G): 
evalfstart(A,B,C,D,E,F,G):[39]: 4  with precondition: [0>=D] 
evalfstart(A,B,C,D,E,F,G):[40]: nat(1*D+1*G)+max([3*D,1*D*nat(nat(1*G)+3)])+4  with precondition: [D>=1] 
Maximum cost of evalfstart(A,B,C,D,E,F,G): max([4,nat(1*D+1*G)+max([3*D,1*D*nat(nat(1*G)+3)])+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 25 ms.
Invariants computed in 82 ms.
----Backward Invariants 41 ms.
----Transitive Invariants 11 ms.
Refinement performed in 64 ms.
Termination proved in 39 ms.
Upper bounds computed in 201 ms.
----Phase cost structures 91 ms.
--------Equation cost structures 64 ms.
--------Inductive compression(1) 16 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 103 ms.
----Solving cost expressions 1 ms.

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