warning: Ignored call to evalaxstop/3 in equation evalaxreturnin/3 
Inferred cost of evalaxbb2in(A,B,C,D,E,F,G): 
evalaxbb2in(A,B,C,D,E,F,G):[21]: 1
  with precondition: [B=0,D=0,F=0,E=A,C=G,1>=C] 

evalaxbb2in(A,B,C,D,E,F,G):[[20],21]: 1+it1*(2)
  Such that:it1=<1*F,it1=<1*C+ -1,it1=<1*G+ -1,it1=<1*G+ -1*B+ -1
  with precondition: [D=0,G=C,A=E,G=F+1,B>=0,G>=B+2] 

Inferred cost of evalaxbbin(A,B,C,D,E,F,G): 
evalaxbbin(A,B,C,D,E,F,G):[25]: 2+it1*(2)
  Such that:it1=<1
  with precondition: [A=0,C=2,D=1,E=0,F=1,G=2] 

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

evalaxbbin(A,B,C,D,E,F,G):[27]: 3+it1*(2)
  Such that:it1=<1
  with precondition: [A=0,C=2,D=0,E=0,F=1,G=2] 

evalaxbbin(A,B,C,D,E,F,G):[29]: 2+it1*(2)
  Such that:it1=<1*F,it1=<1*C+ -1,it1=<1*G+ -1
  with precondition: [A=0,D=1,E=0,C=F+1,C=G,C>=3] 

evalaxbbin(A,B,C,D,E,F,G):[[24],27]: 3+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<1*F,it1=<1*C+ -1,it1=<1*E+1,it1=<1*G+ -1,it2=<1*E,it2=<1*C+ -2,it2=<1*F+ -1,it2=<1*G+ -2,it2=<1*C+ -1*A+ -2
            it3=<1*C+ -1
  with precondition: [D=0,F+1=C,F=E+1,F+1=G,A>=0,F>=A+2] 

evalaxbbin(A,B,C,D,E,F,G):[[24],29]: 2+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<1*F,it1=<1*C+ -1,it1=<1*G+ -1,it2=<1*E,it2=<1*C+ -3,it2=<1*C+ -2,it2=<1*E+ -1*A,it2=<1*F+ -2,it2=<1*F+ -1,it2=<1*G+ -3,it2=<1*G+ -2,it2=<1*G+ -1*A+ -2
            it3=<1*C+ -1
  with precondition: [D=1,C=F+1,C=G,A>=0,E>=A+1,C>=E+3] 

Inferred cost of evalaxreturnin(A,B,C): 
evalaxreturnin(A,B,C):[31]: 1
  with precondition: [] 

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

Inferred cost of evalaxentryin(A,B,C): 
evalaxentryin(A,B,C):[35]: 5
  with precondition: [1>=C] 

evalaxentryin(A,B,C):[36]: 5+it1*(2)
  Such that:it1=<1
  with precondition: [C=2] 

evalaxentryin(A,B,C):[37]: 5+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<1*C+ -1,it2=<1*C+ -2
            it3=<1*C+ -1
  with precondition: [C>=3] 

evalaxentryin(A,B,C):[38]: 3+it1*(2)
  Such that:it1=<1
  with precondition: [C=2] 

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

evalaxentryin(A,B,C):[40]: 3+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<1*C+ -1,it2=<1*C+ -3,it2=<1*C+ -2
            it3=<1*C+ -1
  with precondition: [C>=4] 

Inferred cost of evalaxstart(A,B,C): 
evalaxstart(A,B,C):[42]: 6
  with precondition: [1>=C] 

evalaxstart(A,B,C):[43]: 6+it1*(2)
  Such that:it1=<1
  with precondition: [C=2] 

evalaxstart(A,B,C):[44]: 6+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<1*C+ -1,it2=<1*C+ -2
            it3=<1*C+ -1
  with precondition: [C>=3] 

evalaxstart(A,B,C):[45]: 4+it1*(2)
  Such that:it1=<1
  with precondition: [C=2] 

evalaxstart(A,B,C):[46]: 4+it1*(2)
  Such that:it1=<1*C+ -1
  with precondition: [C>=3] 

evalaxstart(A,B,C):[47]: 4+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<1*C+ -1,it2=<1*C+ -3,it2=<1*C+ -2
            it3=<1*C+ -1
  with precondition: [C>=4] 

Solved cost expressions of evalaxstart(A,B,C): 
evalaxstart(A,B,C):[42]: 6  with precondition: [1>=C] 
evalaxstart(A,B,C):[43]: 8  with precondition: [C=2] 
evalaxstart(A,B,C):[44]: 2*C+ -2+ (2*C+1)* (1*C+ -2)+6  with precondition: [C>=3] 
evalaxstart(A,B,C):[45]: 6  with precondition: [C=2] 
evalaxstart(A,B,C):[46]: 2*C+2  with precondition: [C>=3] 
evalaxstart(A,B,C):[47]: 2*C+ -2+ (2*C+1)* (1*C+ -3)+4  with precondition: [C>=4] 
Maximum cost of evalaxstart(A,B,C): max([2*C+2,8,2*C+ -2+ (2*C+1)* (1*C+ -3)+4,2*C+ -2+ (2*C+1)* (1*C+ -2)+6]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 14 ms.
Invariants computed in 30 ms.
----Backward Invariants 12 ms.
----Transitive Invariants 3 ms.
Refinement performed in 33 ms.
Termination proved in 9 ms.
Upper bounds computed in 135 ms.
----Phase cost structures 50 ms.
--------Equation cost structures 44 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 78 ms.
----Solving cost expressions 1 ms.

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