warning: Ignored call to evalrsdstop/3 in equation evalrsdreturnin/3 
Inferred cost of evalrsdbb4in(A,B,C,D,E,F,G): 
evalrsdbb4in(A,B,C,D,E,F,G):[[17,18],19]: 1+it1*(3)+it2*(3)
  Such that:it1=<nat(min([1*B+1,2*A+1,2*C+1,2*E+1,2*F+3,2*G+3]))*min([1*A,1*B,1*C,1*E,1*F+1,1*G+1])+min([-1*G+1*B,1*C+ -1*G,1*E+1,1*F+2,1*G+2,1*C+ -1*A+1]),it1=<nat(min([1*B+1,2*A+1,2*C+1,2*E+1,2*F+3,2*G+3]))*min([1*B,2*A,2*C,2*E,2*F+2,2*G+2])+min([1*B+1,1*C+1,2*A+1,2*E+1,2*F+3,2*G+3]),it2=<1*A+1,it2=<1*B+1,it2=<1*B+ -1*F,it2=<1*C+1,it2=<1*E+1,it2=<1*F+2,it2=<1*G+2,it2=<2*A+1,it2=<2*C+1,it2=<2*E+1,it2=<2*F+3,it2=<2*G+3,it2=<-1*F+2*G+2,it2=<1*B+ -1*A+1,it2=<1*B+ -1*E+1
  with precondition: [D=0,G+1=A,G+1=E,2*G+2>=B,B>=C,B>=F,C>=G+1,F>=G] 

Inferred cost of evalrsdreturnin(A,B,C): 
evalrsdreturnin(A,B,C):[21]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalrsdbb4in(A,B,C): 
loop_cont_evalrsdbb4in(A,B,C):[23]: 1
  with precondition: [] 

Inferred cost of evalrsdbbin(A,B,C): 
evalrsdbbin(A,B,C):[25]: 3+it1*(3)+it2*(3)
  Such that:it1=<nat(min([2*A+1,2*A+1,4*A+1,2*A+1,4*A+3,2*A+1]))*min([1*A,2*A,2*A,1*A,2*A+1,1*A])+min([1*A+1,1*A+1,1*A+1,2*A+2,1*A+1,1*A+1]),it1=<nat(min([2*A+1,2*A+1,4*A+1,2*A+1,4*A+3,2*A+1]))*min([2*A,2*A,4*A,2*A,4*A+2,2*A])+min([2*A+1,2*A+1,2*A+1,2*A+1,4*A+3,2*A+1]),it2=<1*A+1,it2=<2*A+1,it2=<2*A+2,it2=<4*A+1,it2=<4*A+3
  with precondition: [A>=0] 

Inferred cost of evalrsdentryin(A,B,C): 
evalrsdentryin(A,B,C):[27]: 4+it1*(3)+it2*(3)
  Such that:it1=<nat(min([2*A+1,2*A+1,4*A+1,2*A+1,4*A+3,2*A+1]))*min([1*A,2*A,2*A,1*A,2*A+1,1*A])+min([1*A+1,1*A+1,1*A+1,2*A+2,1*A+1,1*A+1]),it1=<nat(min([2*A+1,2*A+1,4*A+1,2*A+1,4*A+3,2*A+1]))*min([2*A,2*A,4*A,2*A,4*A+2,2*A])+min([2*A+1,2*A+1,2*A+1,2*A+1,4*A+3,2*A+1]),it2=<1*A+1,it2=<2*A+1,it2=<2*A+2,it2=<4*A+1,it2=<4*A+3
  with precondition: [A>=0] 

evalrsdentryin(A,B,C):[28]: 2
  with precondition: [0>=A+1] 

Inferred cost of evalrsdstart(A,B,C): 
evalrsdstart(A,B,C):[30]: 5+it1*(3)+it2*(3)
  Such that:it1=<nat(min([2*A+1,2*A+1,4*A+1,2*A+1,4*A+3,2*A+1]))*min([1*A,2*A,2*A,1*A,2*A+1,1*A])+min([1*A+1,1*A+1,1*A+1,2*A+2,1*A+1,1*A+1]),it1=<nat(min([2*A+1,2*A+1,4*A+1,2*A+1,4*A+3,2*A+1]))*min([2*A,2*A,4*A,2*A,4*A+2,2*A])+min([2*A+1,2*A+1,2*A+1,2*A+1,4*A+3,2*A+1]),it2=<1*A+1,it2=<2*A+1,it2=<2*A+2,it2=<4*A+1,it2=<4*A+3
  with precondition: [A>=0] 

evalrsdstart(A,B,C):[31]: 3
  with precondition: [0>=A+1] 

Solved cost expressions of evalrsdstart(A,B,C): 
evalrsdstart(A,B,C):[30]: 3*A+3+nat(min([1*A+1+ (2*A+1)* (1*A),2*A+1+ (2*A+1)* (2*A)]))*3+5  with precondition: [A>=0] 
evalrsdstart(A,B,C):[31]: 3  with precondition: [0>=A+1] 
Maximum cost of evalrsdstart(A,B,C): max([3,3*A+3+nat(min([1*A+1+ (2*A+1)* (1*A),2*A+1+ (2*A+1)* (2*A)]))*3+5]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 7 ms.
Invariants computed in 15 ms.
----Backward Invariants 6 ms.
----Transitive Invariants 2 ms.
Refinement performed in 15 ms.
Termination proved in 6 ms.
Upper bounds computed in 89 ms.
----Phase cost structures 50 ms.
--------Equation cost structures 45 ms.
--------Inductive compression(1) 1 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 32 ms.
----Solving cost expressions 1 ms.

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