warning: Ignored call to evalfstop/7 in equation evalfreturnin/7 
Inferred cost of evalfbb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
evalfbb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[26]: 1
  with precondition: [H=0,I=A,G=C,L=D,B=J,G=K,E=M,F=N,G=O,G>=E+1,B>=F] 

evalfbb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[25],27]...: inf
  with precondition: [1>=H,H>=0,B>=F,C>=G,E>=G] 

Inferred cost of evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[29]: 1
  with precondition: [H=0,K=C,D=F,O=G,A=I,B=J,D=L,E=M,D=N,D>=B+1,A>=E] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[30]...: inf
  with precondition: [F=D,1>=H,H>=0,E>=C,A>=E,B>=F] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[31]...: inf
  with precondition: [H=1,F=D,E>=C,A>=E,B>=F] 

evalfbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[28],29]: 1+it1*(3)
  Such that:it1=<-1*D+1*N,it1=<-1*L+1*N,it1=<1*N+ -1*F,it1=<-1*L+1*J+1,it1=<1*B+ -1*F+1
  with precondition: [H=0,K=C,A=I,B=J,D=L,E=M,B+1=N,K=O,F>=D,A>=E,K>=E+1,B>=F] 

Inferred cost of evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[35]: 1
  with precondition: [E=1,H=0,M=1,J=B,K=C,N=F,O=G,A=I,D=L,0>=A,D>=1] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[36]...: inf
  with precondition: [E=1,1>=C,1>=H,A>=1,D>=1,H>=0,B>=D] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[37]...: inf
  with precondition: [E=1,H=1,1>=C,A>=1,D>=1,B>=D] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[38]...: inf
  with precondition: [E=1,H=1,1>=C,A>=1,D>=1,B>=D] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],35]: 1+it1*(3)
  Such that:it1=<1*I,it1=<1*M+ -1,it1=<1*A+ -1*E+1,it1=<1*I+ -1*E+1
  with precondition: [H=0,A=I,B=J,C=K,D=L,A+1=M,D=N,G=O,D>=1,E>=1,D>=B+1,A>=E] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],35]: 1+it1*(3+it2*(3))
  Such that:it1=<1*I,it1=<1*C+ -1,it1=<1*K+ -1,it1=<1*M+ -1,it1=<1*M+ -1*E,it1=<1*O+ -1,it1=<1*O+ -1*E,it1=<1*A+ -1*E+1
            it2=<1*B+ -1*D+1,it2=<1*B
  with precondition: [H=0,A=I,B=J,C=K,D=L,A+1=M,B+1=N,C=O,D>=1,E>=1,C>=A+1,B>=D,A>=E] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],36]...: inf
  with precondition: [1>=H,D>=1,E>=1,H>=0,A>=C,B>=D,C>=E+1] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],37]...: inf
  with precondition: [H=1,D>=1,E>=1,A>=C,B>=D,C>=E+1] 

evalfbb8in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[34],38]...: inf
  with precondition: [H=1,D>=1,E>=1,A>=C,B>=D,C>=E+1] 

Inferred cost of evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[43]: 1
  with precondition: [H=0,I=A,J=B,K=C,M=E,N=F,O=G,D=L,0>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[44]...: inf
  with precondition: [1>=C,1>=H,A>=1,D>=1,H>=0,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[45]...: inf
  with precondition: [1>=H,C>=2,D>=1,H>=0,A>=C,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[46]...: inf
  with precondition: [H=1,1>=C,A>=1,D>=1,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[47]...: inf
  with precondition: [H=1,1>=C,A>=1,D>=1,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[48]...: inf
  with precondition: [H=1,1>=C,A>=1,D>=1,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[49]...: inf
  with precondition: [H=1,C>=2,D>=1,A>=C,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[50]...: inf
  with precondition: [H=1,C>=2,D>=1,A>=C,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[51]...: inf
  with precondition: [H=1,C>=2,D>=1,A>=C,B>=D] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[40],43]: 1+it1*(3)
  Such that:it1=<1*D
  with precondition: [H=0,L=0,M=1,A=I,B=J,C=K,F=N,G=O,0>=A,D>=1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],[42],43]: 1+it1*(3+it2*(3+it3*(3)))+it4*(3+it5*(3))
  Such that:it1=<1*B,it1=<1*J,it1=<1*D+ -1,it1=<1*N+ -1,it4=<1*D,it4=<1*D+ -1*B,it4=<1*D+ -1*J
            it2=<1*C+ -1,it2=<1*A
            it3=<1*D+ -1,it3=<1*B
            it5=<1*A
  with precondition: [H=0,L=0,A=I,B=J,C=K,A+1=M,B+1=N,C=O,A>=1,B>=1,C>=A+1,D>=B+1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],43]: 1+it1*(3+it2*(3))
  Such that:it1=<1*D,it1=<1*D+ -1*B,it1=<1*D+ -1*J
            it2=<1*A
  with precondition: [H=0,L=0,N=1,A=I,B=J,C=K,A+1=M,G=O,0>=B,A>=1,D>=1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],44]...: inf
  with precondition: [1>=C,1>=H,A>=1,B>=1,H>=0,D>=B+1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],45]...: inf
  with precondition: [1>=H,B>=1,C>=2,H>=0,D>=B+1,A>=C] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],46]...: inf
  with precondition: [H=1,1>=C,A>=1,B>=1,D>=B+1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],47]...: inf
  with precondition: [H=1,1>=C,A>=1,B>=1,D>=B+1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],48]...: inf
  with precondition: [H=1,1>=C,A>=1,B>=1,D>=B+1] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],49]...: inf
  with precondition: [H=1,B>=1,C>=2,D>=B+1,A>=C] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],50]...: inf
  with precondition: [H=1,B>=1,C>=2,D>=B+1,A>=C] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],51]...: inf
  with precondition: [H=1,B>=1,C>=2,D>=B+1,A>=C] 

evalfbb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[42],43]: 1+it1*(3+it2*(3+it3*(3)))
  Such that:it1=<1*B,it1=<1*D,it1=<1*J,it1=<1*N+ -1
            it2=<1*C+ -1,it2=<1*A
            it3=<1*B
  with precondition: [H=0,L=0,A=I,B=J,C=K,A+1=M,B+1=N,C=O,A>=1,D>=1,C>=A+1,B>=D] 

Inferred cost of evalfreturnin(A,B,C,D,E,F,G): 
evalfreturnin(A,B,C,D,E,F,G):[53]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalfbb10in(A,B,C,D,E,F,G): 
loop_cont_evalfbb10in(A,B,C,D,E,F,G):[55]: 1
  with precondition: [] 

Inferred cost of evalfentryin(A,B,C,D,E,F,G): 
evalfentryin(A,B,C,D,E,F,G):[57]: 3
  with precondition: [0>=A] 

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

evalfentryin(A,B,C,D,E,F,G):[59]: 3+it1*(3+it2*(3+it3*(3)))+it4*(3+it5*(3))
  Such that:it1=<1*C,it1=<1*A+ -1,it4=<1*A,it4=<1*A+ -1*C
            it2=<1*D+ -1,it2=<1*B
            it3=<1*A+ -1,it3=<1*C
            it5=<1*D+ -1,it5=<1*B
  with precondition: [B>=1,C>=1,D>=B+1,A>=C+1] 

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

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

evalfentryin(A,B,C,D,E,F,G):[62]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfentryin(A,B,C,D,E,F,G):[63]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[64]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfentryin(A,B,C,D,E,F,G):[65]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[66]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfentryin(A,B,C,D,E,F,G):[67]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[68]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfentryin(A,B,C,D,E,F,G):[69]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfentryin(A,B,C,D,E,F,G):[70]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfentryin(A,B,C,D,E,F,G):[71]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[72]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[73]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[74]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfentryin(A,B,C,D,E,F,G):[75]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[76]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfentryin(A,B,C,D,E,F,G):[77]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfentryin(A,B,C,D,E,F,G):[78]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfentryin(A,B,C,D,E,F,G):[79]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[80]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfentryin(A,B,C,D,E,F,G):[81]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

Inferred cost of evalfstart(A,B,C,D,E,F,G): 
evalfstart(A,B,C,D,E,F,G):[83]: 4
  with precondition: [0>=A] 

evalfstart(A,B,C,D,E,F,G):[84]: 4+it1*(3)
  Such that:it1=<1*A
  with precondition: [0>=B,A>=1] 

evalfstart(A,B,C,D,E,F,G):[85]: 4+it1*(3+it2*(3+it3*(3)))+it4*(3+it5*(3))
  Such that:it1=<1*C,it1=<1*A+ -1,it4=<1*A,it4=<1*A+ -1*C
            it2=<1*D+ -1,it2=<1*B
            it3=<1*A+ -1,it3=<1*C
            it5=<1*D+ -1,it5=<1*B
  with precondition: [B>=1,C>=1,D>=B+1,A>=C+1] 

evalfstart(A,B,C,D,E,F,G):[86]: 4+it1*(3+it2*(3))
  Such that:it1=<1*A,it1=<1*A+ -1*C
            it2=<1*B
  with precondition: [0>=C,A>=1,B>=1] 

evalfstart(A,B,C,D,E,F,G):[87]: 4+it1*(3+it2*(3+it3*(3)))
  Such that:it1=<1*A,it1=<1*C
            it2=<1*D+ -1,it2=<1*B
            it3=<1*C
  with precondition: [A>=1,B>=1,C>=A,D>=B+1] 

evalfstart(A,B,C,D,E,F,G):[88]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfstart(A,B,C,D,E,F,G):[89]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfstart(A,B,C,D,E,F,G):[90]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfstart(A,B,C,D,E,F,G):[91]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfstart(A,B,C,D,E,F,G):[92]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfstart(A,B,C,D,E,F,G):[93]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfstart(A,B,C,D,E,F,G):[94]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfstart(A,B,C,D,E,F,G):[95]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfstart(A,B,C,D,E,F,G):[96]...: inf
  with precondition: [1>=D,A>=1,B>=1,C>=A] 

evalfstart(A,B,C,D,E,F,G):[97]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfstart(A,B,C,D,E,F,G):[98]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfstart(A,B,C,D,E,F,G):[99]...: inf
  with precondition: [A>=1,D>=2,C>=A,B>=D] 

evalfstart(A,B,C,D,E,F,G):[100]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfstart(A,B,C,D,E,F,G):[101]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfstart(A,B,C,D,E,F,G):[102]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfstart(A,B,C,D,E,F,G):[103]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfstart(A,B,C,D,E,F,G):[104]...: inf
  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 

evalfstart(A,B,C,D,E,F,G):[105]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfstart(A,B,C,D,E,F,G):[106]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

evalfstart(A,B,C,D,E,F,G):[107]...: inf
  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 

Solved cost expressions of evalfstart(A,B,C,D,E,F,G): 
evalfstart(A,B,C,D,E,F,G):[83]: 4  with precondition: [0>=A] 
evalfstart(A,B,C,D,E,F,G):[84]: 3*A+4  with precondition: [0>=B,A>=1] 
evalfstart(A,B,C,D,E,F,G):[85]: (3*B+3)* (1*A+ -1*C)+1*C*nat((3*C+3)* (1*B)+3)+4  with precondition: [B>=1,C>=1,D>=B+1,A>=C+1] 
evalfstart(A,B,C,D,E,F,G):[86]: (3*B+3)* (1*A)+4  with precondition: [0>=C,A>=1,B>=1] 
evalfstart(A,B,C,D,E,F,G):[87]: 1*A*nat((3*C+3)* (1*B)+3)+4  with precondition: [A>=1,B>=1,C>=A,D>=B+1] 
evalfstart(A,B,C,D,E,F,G):[88]...: inf  with precondition: [1>=D,A>=1,B>=1,C>=A] 
evalfstart(A,B,C,D,E,F,G):[89]...: inf  with precondition: [A>=1,D>=2,C>=A,B>=D] 
evalfstart(A,B,C,D,E,F,G):[90]...: inf  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 
evalfstart(A,B,C,D,E,F,G):[91]...: inf  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 
evalfstart(A,B,C,D,E,F,G):[92]...: inf  with precondition: [1>=D,A>=1,B>=1,C>=A] 
evalfstart(A,B,C,D,E,F,G):[93]...: inf  with precondition: [A>=1,D>=2,C>=A,B>=D] 
evalfstart(A,B,C,D,E,F,G):[94]...: inf  with precondition: [1>=D,A>=1,B>=1,C>=A] 
evalfstart(A,B,C,D,E,F,G):[95]...: inf  with precondition: [1>=D,A>=1,B>=1,C>=A] 
evalfstart(A,B,C,D,E,F,G):[96]...: inf  with precondition: [1>=D,A>=1,B>=1,C>=A] 
evalfstart(A,B,C,D,E,F,G):[97]...: inf  with precondition: [A>=1,D>=2,C>=A,B>=D] 
evalfstart(A,B,C,D,E,F,G):[98]...: inf  with precondition: [A>=1,D>=2,C>=A,B>=D] 
evalfstart(A,B,C,D,E,F,G):[99]...: inf  with precondition: [A>=1,D>=2,C>=A,B>=D] 
evalfstart(A,B,C,D,E,F,G):[100]...: inf  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 
evalfstart(A,B,C,D,E,F,G):[101]...: inf  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 
evalfstart(A,B,C,D,E,F,G):[102]...: inf  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 
evalfstart(A,B,C,D,E,F,G):[103]...: inf  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 
evalfstart(A,B,C,D,E,F,G):[104]...: inf  with precondition: [1>=D,B>=1,C>=1,A>=C+1] 
evalfstart(A,B,C,D,E,F,G):[105]...: inf  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 
evalfstart(A,B,C,D,E,F,G):[106]...: inf  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 
evalfstart(A,B,C,D,E,F,G):[107]...: inf  with precondition: [C>=1,D>=2,A>=C+1,B>=D] 
Maximum cost of evalfstart(A,B,C,D,E,F,G): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 37 ms.
Invariants computed in 238 ms.
----Backward Invariants 141 ms.
----Transitive Invariants 21 ms.
Refinement performed in 167 ms.
Termination proved in 50 ms.
Upper bounds computed in 385 ms.
----Phase cost structures 146 ms.
--------Equation cost structures 115 ms.
--------Inductive compression(1) 1 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 214 ms.
----Solving cost expressions 4 ms.

Compressed phase information: 22 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 933 ms.