warning: Ignored call to evalEx2stop/4 in equation evalEx2returnin/4 
Inferred cost of evalEx2bb2in(A,B,C,D,E,F,G,H,I): 
evalEx2bb2in(A,B,C,D,E,F,G,H,I):[21]: 1
  with precondition: [E=0,A=C+1,B=D+1,A=F+1,B=G+1,A=H+1,B=I+1,A>=1,B>=1] 

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

evalEx2bb2in(A,B,C,D,E,F,G,H,I):[[20],22]...: inf
  with precondition: [A+B=C+D+2,1>=E,A>=1,B>=1,E>=0,C+1>=A] 

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

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[26]: 0
  with precondition: [E=1,F=A,H=C,I=D,B=G,B>=1] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[27]: 1
  with precondition: [E=0,G=B,H=C,I=D,A=F,0>=A] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[28]: 0
  with precondition: [E=1,G=B,H=C,I=D,A=F,A>=1] 

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

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

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[[23,24],25]: 1+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*B,it1+it2=<1*B+ -1*G,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<1/2*A+1/2*B+ -1/2*F+ -1/2*G,it1+it2=<1/2*F+1/2*G+1*B+ -1/2
  with precondition: [E=0,H=F,I=G,0>=I,A>=1,H+I>=0,B+H+I>=A,A+B>=H+I+2] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[[23,24],26]: 0+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*B,it1+it2=<-1*I+1*B,it1+it2=<1*B+ -1*G,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<-1/2*I+1/2*H+1*B+ -1/2,it1+it2=<1/2*A+1/2*B+ -1/2*F+ -1/2*I
  with precondition: [E=1,F=H,G=I,A>=1,F>=0,G>=1,B+F>=A+G,A+B>=F+G+2] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[[23,24],27]: 1+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*B,it1+it2=<-1*G+1*B,it1+it2=<1*B+ -1*I,it1+it2=<-1/2*G+1*B+ -1/2,it1+it2=<1/2*A+1/2*B+ -1/2*I,it1+it2=<1/2*A+1/2*B+ -1/2
  with precondition: [E=0,F=0,H=0,G=I,A>=1,G>=0,B>=A+G] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[[23,24],28]: 0+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*B,it1+it2=<-1*I+1*B,it1+it2=<1*B+ -1*G,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<-1/2*I+1/2*F+1*B+ -1/2,it1+it2=<1/2*A+1/2*B+ -1/2*F+ -1/2*G,it1+it2=<1/2*F+1/2*I+1*B+ -1/2
  with precondition: [E=1,H=F,I=G,A>=1,H>=1,H+I>=0,B+H>=A+I,B+H+I>=A,A+B>=H+I+2] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[[23,24],29]...: inf
  with precondition: [1>=E,A>=1,B>=2,E>=0,A+B>=4] 

evalEx2bb3in(A,B,C,D,E,F,G,H,I):[[23,24],30]...: inf
  with precondition: [E=1,A>=1,B>=2,A+B>=4] 

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

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

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

evalEx2entryin(A,B,C,D):[37]: 3
  with precondition: [0>=B] 

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

evalEx2entryin(A,B,C,D):[39]: 3+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1*A+ -1/2,it1+it2=<1/2*A+1/2*B,it1+it2=<1/2*A+1/2*B+ -1/2
  with precondition: [B>=1,A>=B] 

evalEx2entryin(A,B,C,D):[40]: 1
  with precondition: [A>=1] 

evalEx2entryin(A,B,C,D):[41]: 1
  with precondition: [B>=1] 

evalEx2entryin(A,B,C,D):[42]: 1+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1*A+ -1,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<1/2*B+3/2*A+ -5/2
  with precondition: [A>=2,B>=1] 

evalEx2entryin(A,B,C,D):[43]: 1+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1/2*A+1/2*B,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<1/2*B+3/2*A+ -3/2
  with precondition: [A>=1,B>=1] 

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

evalEx2entryin(A,B,C,D):[45]...: inf
  with precondition: [A>=2,B>=1,A+B>=4] 

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

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

evalEx2entryin(A,B,C,D):[48]...: inf
  with precondition: [A>=2,B>=1,A+B>=4] 

evalEx2entryin(A,B,C,D):[49]...: inf
  with precondition: [A>=2,B>=1,A+B>=4] 

Inferred cost of evalEx2start(A,B,C,D): 
evalEx2start(A,B,C,D):[51]: 4
  with precondition: [0>=A] 

evalEx2start(A,B,C,D):[52]: 4
  with precondition: [0>=B] 

evalEx2start(A,B,C,D):[53]: 4+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1/2*A+1/2*B,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<3/2*A+1/2*B+ -3/2
  with precondition: [A>=1,B>=1] 

evalEx2start(A,B,C,D):[54]: 4+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1*A+ -1/2,it1+it2=<1/2*A+1/2*B,it1+it2=<1/2*A+1/2*B+ -1/2
  with precondition: [B>=1,A>=B] 

evalEx2start(A,B,C,D):[55]: 2
  with precondition: [A>=1] 

evalEx2start(A,B,C,D):[56]: 2
  with precondition: [B>=1] 

evalEx2start(A,B,C,D):[57]: 2+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1*A+ -1,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<3/2*A+1/2*B+ -5/2
  with precondition: [A>=2,B>=1] 

evalEx2start(A,B,C,D):[58]: 2+it1*(3)+it2*(inf)
  Such that:it1+it2=<1*A,it1+it2=<1/2*A+1/2*B,it1+it2=<1/2*A+1/2*B+ -1/2,it1+it2=<3/2*A+1/2*B+ -3/2
  with precondition: [A>=1,B>=1] 

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

evalEx2start(A,B,C,D):[60]...: inf
  with precondition: [A>=2,B>=1,A+B>=4] 

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

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

evalEx2start(A,B,C,D):[63]...: inf
  with precondition: [A>=2,B>=1,A+B>=4] 

evalEx2start(A,B,C,D):[64]...: inf
  with precondition: [A>=2,B>=1,A+B>=4] 

Solved cost expressions of evalEx2start(A,B,C,D): 
evalEx2start(A,B,C,D):[51]: 4  with precondition: [0>=A] 
evalEx2start(A,B,C,D):[52]: 4  with precondition: [0>=B] 
evalEx2start(A,B,C,D):[53]: inf  with precondition: [A>=1,B>=1] 
evalEx2start(A,B,C,D):[54]: inf  with precondition: [B>=1,A>=B] 
evalEx2start(A,B,C,D):[55]: 2  with precondition: [A>=1] 
evalEx2start(A,B,C,D):[56]: 2  with precondition: [B>=1] 
evalEx2start(A,B,C,D):[57]: inf  with precondition: [A>=2,B>=1] 
evalEx2start(A,B,C,D):[58]: inf  with precondition: [A>=1,B>=1] 
evalEx2start(A,B,C,D):[59]...: inf  with precondition: [A>=1,B>=1] 
evalEx2start(A,B,C,D):[60]...: inf  with precondition: [A>=2,B>=1,A+B>=4] 
evalEx2start(A,B,C,D):[61]...: inf  with precondition: [A>=1,B>=1] 
evalEx2start(A,B,C,D):[62]...: inf  with precondition: [A>=1,B>=1] 
evalEx2start(A,B,C,D):[63]...: inf  with precondition: [A>=2,B>=1,A+B>=4] 
evalEx2start(A,B,C,D):[64]...: inf  with precondition: [A>=2,B>=1,A+B>=4] 
Maximum cost of evalEx2start(A,B,C,D): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 13 ms.
Invariants computed in 72 ms.
----Backward Invariants 48 ms.
----Transitive Invariants 5 ms.
Refinement performed in 54 ms.
Termination proved in 11 ms.
Upper bounds computed in 124 ms.
----Phase cost structures 38 ms.
--------Equation cost structures 35 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 70 ms.
----Solving cost expressions 6 ms.

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