warning: Ignored call to loop_cont_eval1/3 in equation start/3 
Inferred cost of eval2(A,B,C,D,E,F,G): 
eval2(A,B,C,D,E,F,G):[13]: 1
  with precondition: [D=0,A=E+1,B=F,C=G,A>=B+1,B>=C] 

eval2(A,B,C,D,E,F,G):[14]: 0
  with precondition: [D=1,G=C,A=E,B=F,A>=B+1] 

eval2(A,B,C,D,E,F,G):[[12],13]: 1+it1*(1)
  Such that:it1=<1*C+ -1*G
  with precondition: [D=0,G=B,A=E+1,G=F,A>=G+1,C>=G+1] 

eval2(A,B,C,D,E,F,G):[[12],14]: 0+it1*(1)
  Such that:it1=<1*C+ -1*F,it1=<1*C+ -1*G
  with precondition: [D=1,A=E,B=F,A>=B+1,G>=B,C>=G+1] 

Inferred cost of eval1(A,B,C,D,E,F,G): 
eval1(A,B,C,D,E,F,G):[18]: 1
  with precondition: [D=1,A>=B+1] 

eval1(A,B,C,D,E,F,G):[19]: 1+it1*(1)
  Such that:it1=<-1*B+1*C,it1=<1*C+ -1*B
  with precondition: [D=1,A>=B+1,C>=B+1] 

eval1(A,B,C,D,E,F,G):[20]: 0
  with precondition: [D=1,E=A,F=B,G=C] 

eval1(A,B,C,D,E,F,G):[[16],18]: 1+it1*(2)
  Such that:it1=<1*A+ -1*B,it1=<1*A+ -1*C,it1=<-1*B+1*A+ -1
  with precondition: [D=1,A>=B+2,B>=C] 

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

eval1(A,B,C,D,E,F,G):[17,[16],18]: 3+it1*(2)+it2*(1)
  Such that:it1=<1*A+ -1*B+ -2,it1=<1*A+ -1*B+ -1,it2=<1*C+ -1*B
  with precondition: [D=1,A>=B+3,C>=B+1] 

eval1(A,B,C,D,E,F,G):[17,[16],20]: 2+it1*(2)+it2*(1)
  Such that:it1=<1*A+ -1*E+ -1,it1=<1*A+ -1*F+ -1,it2=<1*C+ -1*G
  with precondition: [D=1,B=F,B=G,C>=B+1,E>=B,A>=E+2] 

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

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

Inferred cost of start(A,B,C): 
start(A,B,C):[22]: 2
  with precondition: [A>=B+1] 

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

start(A,B,C):[24]: 1
  with precondition: [] 

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

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

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

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

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

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

Solved cost expressions of start(A,B,C): 
start(A,B,C):[22]: 2  with precondition: [A>=B+1] 
start(A,B,C):[23]: -1*B+1*C+2  with precondition: [A>=B+1,C>=B+1] 
start(A,B,C):[24]: 1  with precondition: [] 
start(A,B,C):[25]: 2*A+ -2*B  with precondition: [A>=B+2,B>=C] 
start(A,B,C):[26]: 2*A+ -2*B+1  with precondition: [A>=B+1,B>=C] 
start(A,B,C):[27]: 2*A+ -3*B+1*C  with precondition: [A>=B+3,C>=B+1] 
start(A,B,C):[28]: 2*A+ -3*B+1*C+1  with precondition: [A>=B+2,C>=B+1] 
start(A,B,C):[29]: -1*B+1*C+4  with precondition: [A>=B+2,C>=B+1] 
start(A,B,C):[30]: -1*B+1*C+3  with precondition: [A>=B+1,C>=B+1] 
Maximum cost of start(A,B,C): max([2*A+ -3*B+1*C+1,2,-1*B+1*C+4,2*A+ -2*B+1]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 6 ms.
Invariants computed in 52 ms.
----Backward Invariants 29 ms.
----Transitive Invariants 3 ms.
Refinement performed in 29 ms.
Termination proved in 7 ms.
Upper bounds computed in 98 ms.
----Phase cost structures 22 ms.
--------Equation cost structures 21 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 63 ms.
----Solving cost expressions 3 ms.

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