warning: Ignored call to evalspeedpldi3stop/4 in equation evalspeedpldi3returnin/4 
Inferred cost of evalspeedpldi3bb5in(A,B,C,D,E,F,G,H,I): 
evalspeedpldi3bb5in(A,B,C,D,E,F,G,H,I):[[16,17],18]: 1+it1*(3)+it2*(3)
  Such that:it1=<nat(min([1*G,1*I,1*B+ -1*D,1*G+ -1*D]))*min([1*A,1*F,1*B+ -1,1*G+ -1,1*I+ -1])+min([1*F,1*A+ -1*C,1*B+ -1,1*F+ -1*C,1*G+ -1,1*I+ -1]),it1=<nat(min([1*G,1*I,1*B+ -1*D,1*G+ -1*D]))*min([1*B+ -1,1*G+ -1,1*I+ -1])+min([1*B+ -1,1*G+ -1,1*I+ -1,1*I+ -1*C+ -1]),it2=<1*G,it2=<1*I,it2=<1*B+ -1*D,it2=<1*G+ -1*D,it2=<nat(min([1*G,1*I,1*B+ -1*D,1*G+ -1*D]))*min([1*A,1*F,1*B+ -1,1*G+ -1,1*I+ -1])+min([1*F,1*A+ -1*C,1*B+ -1,1*F+ -1*C,1*G+ -1,1*I+ -1])+1*C
  with precondition: [E=0,H=0,A=F,B=G,B=I,A>=1,C>=0,D>=0,B>=A+1,B>=D+1] 

Inferred cost of evalspeedpldi3returnin(A,B,C,D): 
evalspeedpldi3returnin(A,B,C,D):[20]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalspeedpldi3bb5in(A,B,C,D): 
loop_cont_evalspeedpldi3bb5in(A,B,C,D):[22]: 1
  with precondition: [] 

Inferred cost of evalspeedpldi3entryin(A,B,C,D): 
evalspeedpldi3entryin(A,B,C,D):[24]: 2
  with precondition: [0>=A] 

evalspeedpldi3entryin(A,B,C,D):[25]: 2
  with precondition: [A>=B] 

evalspeedpldi3entryin(A,B,C,D):[26]: 3+it1*(3)+it2*(3)
  Such that:it1=<nat(min([1*B,1*B,1*B,1*B]))*min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1]),it1=<nat(min([1*B,1*B,1*B,1*B]))*min([1*B+ -1,1*B+ -1,1*B+ -1])+min([1*B+ -1,1*B+ -1,1*B+ -1,1*B+ -1]),it2=<1*B,it2=<nat(min([1*B,1*B,1*B,1*B]))*min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1])
  with precondition: [A>=1,B>=A+1] 

Inferred cost of evalspeedpldi3start(A,B,C,D): 
evalspeedpldi3start(A,B,C,D):[28]: 3
  with precondition: [0>=A] 

evalspeedpldi3start(A,B,C,D):[29]: 3
  with precondition: [A>=B] 

evalspeedpldi3start(A,B,C,D):[30]: 4+it1*(3)+it2*(3)
  Such that:it1=<nat(min([1*B,1*B,1*B,1*B]))*min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1]),it1=<nat(min([1*B,1*B,1*B,1*B]))*min([1*B+ -1,1*B+ -1,1*B+ -1])+min([1*B+ -1,1*B+ -1,1*B+ -1,1*B+ -1]),it2=<1*B,it2=<nat(min([1*B,1*B,1*B,1*B]))*min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1])
  with precondition: [A>=1,B>=A+1] 

Solved cost expressions of evalspeedpldi3start(A,B,C,D): 
evalspeedpldi3start(A,B,C,D):[28]: 3  with precondition: [0>=A] 
evalspeedpldi3start(A,B,C,D):[29]: 3  with precondition: [A>=B] 
evalspeedpldi3start(A,B,C,D):[30]: nat(min([1*B* (1*A)+1*A,1*B+ -1+ (1*B+ -1)* (1*B)]))*3+nat(min([1*B,1*B* (1*A)+1*A]))*3+4  with precondition: [A>=1,B>=A+1] 
Maximum cost of evalspeedpldi3start(A,B,C,D): max([3,nat(min([1*B* (1*A)+1*A,1*B+ -1+ (1*B+ -1)* (1*B)]))*3+nat(min([1*B,1*B* (1*A)+1*A]))*3+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 10 ms.
Invariants computed in 21 ms.
----Backward Invariants 9 ms.
----Transitive Invariants 4 ms.
Refinement performed in 20 ms.
Termination proved in 9 ms.
Upper bounds computed in 94 ms.
----Phase cost structures 46 ms.
--------Equation cost structures 42 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 42 ms.
----Solving cost expressions 3 ms.

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