warning: Ignored call to evalEx5stop/5 in equation evalEx5returnin/5 
Inferred cost of evalEx5bb3in(A,B,C,D,E,F,G,H,I,J,K): 
evalEx5bb3in(A,B,C,D,E,F,G,H,I,J,K):[22]: 1
  with precondition: [C=0,F=0,I=0,B=D,K=E,A=G,B=H,B=J,B>=A+1] 

evalEx5bb3in(A,B,C,D,E,F,G,H,I,J,K):[[20,21],22]: inf
  with precondition: [F=0,A=G,B=H,1>=I,C>=0,B>=A+1,I>=C,B>=D,D>=J] 

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

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

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[28]...: inf
  with precondition: [A=0,1>=F,B>=1,F>=0] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[29]...: inf
  with precondition: [A=0,1>=F,B>=1,F>=0] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[30]...: inf
  with precondition: [A=0,1>=F,B>=1,F>=0] 

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

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[[24,25,26],27]: 1+it1*(3)+it2*(inf)
  Such that:it1=<1*B,it1=<1*B+ -1*A,it1=<-1*H+1*B+1*G,it1=<1*B+1*G+ -1*A+ -1*J
  with precondition: [F=0,J=H,1>=I,A>=0,I>=0,G>=J,G+I>=A+1,B>=G+I] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[[24,25,26],28]...: inf
  with precondition: [1>=F,A>=0,F>=0,B>=A+1] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[[24,25,26],29]...: inf
  with precondition: [1>=F,A>=0,F>=0,B>=A+1] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[[24,25,26],30]...: inf
  with precondition: [1>=F,A>=0,F>=0,B>=A+1] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[[24,25,26],31]...: inf
  with precondition: [F=1,A>=0,B>=A+1] 

evalEx5bb6in(A,B,C,D,E,F,G,H,I,J,K):[[24,25,26],32]...: 0+it1*(3)+it2*(inf)
  Such that:it1=<1*B,it1=<1*B+ -1*A
  with precondition: [1>=F,A>=0,F>=0,B>=A+1] 

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

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

Inferred cost of evalEx5entryin(A,B,C,D,E): 
evalEx5entryin(A,B,C,D,E):[37]: 3
  with precondition: [0>=A] 

evalEx5entryin(A,B,C,D,E):[38]: 3+it1*(3)+it2*(inf)
  Such that:it1=<1*A
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[39]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[40]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[41]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[42]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[43]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[44]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[45]...: 1+it1*(3)+it2*(inf)
  Such that:it1=<1*A
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[46]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[47]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[48]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[49]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[50]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[51]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[52]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[53]...: inf
  with precondition: [A>=1] 

evalEx5entryin(A,B,C,D,E):[54]...: 1+it1*(3)+it2*(inf)
  Such that:it1=<1*A
  with precondition: [A>=1] 

Inferred cost of evalEx5start(A,B,C,D,E): 
evalEx5start(A,B,C,D,E):[56]: 4
  with precondition: [0>=A] 

evalEx5start(A,B,C,D,E):[57]: 4+it1*(3)+it2*(inf)
  Such that:it1=<1*A
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[58]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[59]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[60]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[61]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[62]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[63]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[64]...: 2+it1*(3)+it2*(inf)
  Such that:it1=<1*A
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[65]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[66]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[67]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[68]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[69]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[70]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[71]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[72]...: inf
  with precondition: [A>=1] 

evalEx5start(A,B,C,D,E):[73]...: 2+it1*(3)+it2*(inf)
  Such that:it1=<1*A
  with precondition: [A>=1] 

Solved cost expressions of evalEx5start(A,B,C,D,E): 
evalEx5start(A,B,C,D,E):[56]: 4  with precondition: [0>=A] 
evalEx5start(A,B,C,D,E):[57]: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[58]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[59]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[60]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[61]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[62]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[63]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[64]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[65]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[66]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[67]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[68]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[69]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[70]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[71]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[72]...: inf  with precondition: [A>=1] 
evalEx5start(A,B,C,D,E):[73]...: inf  with precondition: [A>=1] 
Maximum cost of evalEx5start(A,B,C,D,E): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 22 ms.
Invariants computed in 81 ms.
----Backward Invariants 50 ms.
----Transitive Invariants 8 ms.
Refinement performed in 70 ms.
Termination proved in 13 ms.
Upper bounds computed in 81 ms.
----Phase cost structures 24 ms.
--------Equation cost structures 24 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 48 ms.
----Solving cost expressions 1 ms.

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