warning: Ignored call to evalNestedMultiplestop/5 in equation evalNestedMultiplereturnin/5 
Inferred cost of evalNestedMultiplebb2in(A,B,C,D,E,F,G,H,I,J,K): 
evalNestedMultiplebb2in(A,B,C,D,E,F,G,H,I,J,K):[19]: 2
  with precondition: [F=0,D=E,A=G,B=H,C=I,D=J,D=K,A>=B+1,C>=D+1] 

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

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

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

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

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

evalNestedMultiplebb5in(A,B,C,D,E,F,G,H,I,J,K):[[22,24],25,[23],26]: 4+it1*(3)+it2*(3)+it3*(4)+it4*(3)
  Such that:it1+it3=<1*A+ -1*B+ -1,it1+it3=<1*G+ -1*B+ -1,it2=<1*C+ -1*D,it2=<1*K+ -1*D,it2+it4=<1*C+ -1*D,it2+it4=<1*K+ -1*D,it3=<1*A+ -1*B,it3=<1*G+ -1*B,it4=<1*C+ -1*D+ -1,it4=<1*J+ -1*D+ -1
  with precondition: [F=0,A=G,A=H,C=I,C=J,C=K,A>=B+3,C>=D+1] 

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

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

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

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

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

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

Inferred cost of evalNestedMultipleentryin(A,B,C,D,E): 
evalNestedMultipleentryin(A,B,C,D,E):[32]: 3
  with precondition: [A>=B] 

evalNestedMultipleentryin(A,B,C,D,E):[33]: 3+it1*(3)
  Such that:it1=<1*B+ -1*A
  with precondition: [B>=A+1,C>=D] 

evalNestedMultipleentryin(A,B,C,D,E):[34]: 6+it1*(3)+it2*(3)+it3*(4)+it4*(3)
  Such that:it1+it3=<1*B+ -1*A+ -1,it2=<1*D+ -1*C,it2+it4=<1*D+ -1*C,it3=<1*B+ -1*A,it4=<1*D+ -1*C+ -1
  with precondition: [B>=A+3,D>=C+1] 

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

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

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

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

Inferred cost of evalNestedMultiplestart(A,B,C,D,E): 
evalNestedMultiplestart(A,B,C,D,E):[40]: 4
  with precondition: [A>=B] 

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

evalNestedMultiplestart(A,B,C,D,E):[42]: 7+it1*(3)+it2*(3)+it3*(4)+it4*(3)
  Such that:it1+it3=<1*B+ -1*A+ -1,it2=<1*D+ -1*C,it2+it4=<1*D+ -1*C,it3=<1*B+ -1*A,it4=<1*D+ -1*C+ -1
  with precondition: [B>=A+3,D>=C+1] 

evalNestedMultiplestart(A,B,C,D,E):[43]: 7+it1*(3)+it2*(4)+it3*(3)
  Such that:it1=<1*D+ -1*C,it1+it3=<1*D+ -1*C,it2=<1*B+ -1*A,it2=<1*B+ -1*A+ -1,it3=<1*D+ -1*C+ -1
  with precondition: [B>=A+2,D>=C+1] 

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

evalNestedMultiplestart(A,B,C,D,E):[45]: 7+it1*(3)+it2*(3)
  Such that:it1=<1*B+ -1*A+ -1,it2=<1*D+ -1*C
  with precondition: [B>=A+2,D>=C+1] 

evalNestedMultiplestart(A,B,C,D,E):[46]: 7+it1*(3)
  Such that:it1=<1*D+ -1*C
  with precondition: [B=A+1,D>=C+1] 

Solved cost expressions of evalNestedMultiplestart(A,B,C,D,E): 
evalNestedMultiplestart(A,B,C,D,E):[40]: 4  with precondition: [A>=B] 
evalNestedMultiplestart(A,B,C,D,E):[41]: -3*A+3*B+4  with precondition: [B>=A+1,C>=D] 
evalNestedMultiplestart(A,B,C,D,E):[42]: -4*A+4*B+ -3*C+3*D+3  with precondition: [B>=A+3,D>=C+1] 
evalNestedMultiplestart(A,B,C,D,E):[43]: -4*A+4*B+ -3*C+3*D+3  with precondition: [B>=A+2,D>=C+1] 
evalNestedMultiplestart(A,B,C,D,E):[44]: -4*A+4*B+ -3*C+3*D+1  with precondition: [B>=A+1,D>=C+1] 
evalNestedMultiplestart(A,B,C,D,E):[45]: -3*A+3*B+ -3*C+3*D+4  with precondition: [B>=A+2,D>=C+1] 
evalNestedMultiplestart(A,B,C,D,E):[46]: -3*C+3*D+7  with precondition: [B=A+1,D>=C+1] 
Maximum cost of evalNestedMultiplestart(A,B,C,D,E): max([-3*A+3*B+ -3*C+3*D+4,-3*A+3*B+4,4,-3*C+3*D+7,-4*A+4*B+ -3*C+3*D+3]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 15 ms.
Invariants computed in 94 ms.
----Backward Invariants 47 ms.
----Transitive Invariants 6 ms.
Refinement performed in 58 ms.
Termination proved in 17 ms.
Upper bounds computed in 316 ms.
----Phase cost structures 65 ms.
--------Equation cost structures 58 ms.
--------Inductive compression(1) 3 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 236 ms.
----Solving cost expressions 3 ms.

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