warning: Ignored call to evalSimpleSingle2stop/4 in equation evalSimpleSingle2returnin/4 
Inferred cost of evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I): 
evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[17]: 3
  with precondition: [A=0,B=0,E=0,F=0,G=0,C=H,D=I,0>=C,0>=D] 

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

evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[[15],[16],17]: 3+it1*(4)+it2*(3)
  Such that:it1=<1*D+ -1,it1=<1*D+ -1*C,it1=<1*D+ -1*H,it1=<1*F+ -1,it1=<1*F+ -1*H,it1=<1*G+ -1,it1=<1*G+ -1*H,it1=<1*I+ -1,it1=<1*I+ -1*H,it1=<-1*A+1*I+ -1,it1=<-1*B+1*I+ -1,it2=<1*C,it2=<1*H,it2=<1*C+ -1*A,it2=<1*C+ -1*B,it2=<1*D+ -1,it2=<1*F+ -1,it2=<1*G+ -1,it2=<1*I+ -1
  with precondition: [E=0,A=B,D=F,D=G,C=H,D=I,A>=0,C>=A+1,D>=C+1] 

evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[[15],[16],18]: 1+it1*(4)+it2*(3)
  Such that:it1=<-1*H+1*D,it1=<-1*H+1*I,it1=<1*D+ -1,it1=<1*D+ -1*H,it1=<1*F+ -1*H,it1=<1*G+ -1*C,it1=<1*G+ -1*H,it1=<1*I+ -1,it1=<1*I+ -1*C,it1=<1*I+ -1*H,it1=<-1*A+1*I+ -1,it1=<-1*B+1*I+ -1,it2=<1*C,it2=<1*H,it2=<1*C+ -1*A,it2=<1*C+ -1*B,it2=<1*D+ -1,it2=<1*F+ -1,it2=<1*G+ -1,it2=<1*I+ -1
  with precondition: [E=0,A=B,F=G,C=H,D=I,A>=0,C>=A+1,F>=C+1,D>=F] 

evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[[15],17]: 3+it1*(3)
  Such that:it1=<1*C,it1=<1*F,it1=<1*G,it1=<1*H,it1=<1*C+ -1*A,it1=<1*C+ -1*B
  with precondition: [E=0,A=B,H=C,H=F,H=G,D=I,A>=0,H>=A+1,H>=D] 

evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[[15],18]: 1+it1*(3)
  Such that:it1=<1*C,it1=<1*F,it1=<1*G,it1=<1*H,it1=<1*G+ -1*A,it1=<1*G+ -1*B,it1=<1*H+ -1*A,it1=<1*H+ -1*B
  with precondition: [E=0,A=B,G=F,C=H,D=I,A>=0,G>=A+1,C>=G] 

evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[[16],17]: 3+it1*(4)
  Such that:it1=<1*D,it1=<1*F,it1=<1*G,it1=<1*I,it1=<-1*C+1*I,it1=<-1*H+1*D,it1=<-1*H+1*F,it1=<1*D+ -1*A,it1=<1*D+ -1*B
  with precondition: [E=0,A=B,G=D,G=F,C=H,G=I,A>=0,G>=A+1,A>=C] 

evalSimpleSingle2bb4in(A,B,C,D,E,F,G,H,I):[[16],18]: 1+it1*(4)
  Such that:it1=<1*D,it1=<1*F,it1=<1*G,it1=<1*I,it1=<-1*C+1*F,it1=<-1*C+1*I,it1=<-1*H+1*D,it1=<-1*H+1*F,it1=<-1*H+1*G,it1=<-1*H+1*I,it1=<1*G+ -1*A,it1=<1*G+ -1*B,it1=<1*I+ -1*A,it1=<1*I+ -1*B
  with precondition: [E=0,A=B,G=F,C=H,D=I,A>=0,G>=A+1,A>=C,D>=G] 

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

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

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

evalSimpleSingle2entryin(A,B,C,D):[25]: 3
  with precondition: [] 

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

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

evalSimpleSingle2entryin(A,B,C,D):[28]: 5+it1*(3)
  Such that:it1=<1*C
  with precondition: [C>=1,C>=D] 

evalSimpleSingle2entryin(A,B,C,D):[29]: 3+it1*(3)
  Such that:it1=<1*C
  with precondition: [C>=1] 

evalSimpleSingle2entryin(A,B,C,D):[30]: 5+it1*(4)
  Such that:it1=<1*D,it1=<1*D+ -1*C
  with precondition: [0>=C,D>=1] 

evalSimpleSingle2entryin(A,B,C,D):[31]: 3+it1*(4)
  Such that:it1=<1*D,it1=<-1*C+1*D,it1=<1*D+ -1*C
  with precondition: [0>=C,D>=1] 

Inferred cost of evalSimpleSingle2start(A,B,C,D): 
evalSimpleSingle2start(A,B,C,D):[33]: 6
  with precondition: [0>=C,0>=D] 

evalSimpleSingle2start(A,B,C,D):[34]: 4
  with precondition: [] 

evalSimpleSingle2start(A,B,C,D):[35]: 6+it1*(4)+it2*(3)
  Such that:it1=<1*D+ -1,it1=<1*D+ -1*C,it2=<1*C,it2=<1*D+ -1
  with precondition: [C>=1,D>=C+1] 

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

evalSimpleSingle2start(A,B,C,D):[37]: 6+it1*(3)
  Such that:it1=<1*C
  with precondition: [C>=1,C>=D] 

evalSimpleSingle2start(A,B,C,D):[38]: 4+it1*(3)
  Such that:it1=<1*C
  with precondition: [C>=1] 

evalSimpleSingle2start(A,B,C,D):[39]: 6+it1*(4)
  Such that:it1=<1*D,it1=<1*D+ -1*C
  with precondition: [0>=C,D>=1] 

evalSimpleSingle2start(A,B,C,D):[40]: 4+it1*(4)
  Such that:it1=<1*D,it1=<1*D+ -1*C
  with precondition: [0>=C,D>=1] 

Solved cost expressions of evalSimpleSingle2start(A,B,C,D): 
evalSimpleSingle2start(A,B,C,D):[33]: 6  with precondition: [0>=C,0>=D] 
evalSimpleSingle2start(A,B,C,D):[34]: 4  with precondition: [] 
evalSimpleSingle2start(A,B,C,D):[35]: -1*C+4*D+6  with precondition: [C>=1,D>=C+1] 
evalSimpleSingle2start(A,B,C,D):[36]: -1*C+4*D+4  with precondition: [C>=1,D>=C+1] 
evalSimpleSingle2start(A,B,C,D):[37]: 3*C+6  with precondition: [C>=1,C>=D] 
evalSimpleSingle2start(A,B,C,D):[38]: 3*C+4  with precondition: [C>=1] 
evalSimpleSingle2start(A,B,C,D):[39]: 4*D+6  with precondition: [0>=C,D>=1] 
evalSimpleSingle2start(A,B,C,D):[40]: 4*D+4  with precondition: [0>=C,D>=1] 
Maximum cost of evalSimpleSingle2start(A,B,C,D): max([-1*C+4*D+6,4*D+6,3*C+6,6]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 11 ms.
Invariants computed in 63 ms.
----Backward Invariants 40 ms.
----Transitive Invariants 4 ms.
Refinement performed in 34 ms.
Termination proved in 11 ms.
Upper bounds computed in 661 ms.
----Phase cost structures 64 ms.
--------Equation cost structures 63 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 585 ms.
----Solving cost expressions 2 ms.

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