warning: Ignored call to f13/18 in equation f0/18 
warning: Ignored call to loop_cont_f17/18 in equation f0/18 
warning: Ignored call to loop_cont_f17/18 in equation f0/18 
Inferred cost of f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1): 
f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[31]: 1
  with precondition: [F=1,S=0,Y=1,B+1=C,W=D,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,B+1=V,E=X,0>=B,0>=E+1,A>=B] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[32]: 0
  with precondition: [F=1,S=1,Y=1,B+1=C,W=D,X=E,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,B+1=V,A>=B] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[33]: 1
  with precondition: [F=1,S=0,Y=1,B+1=C,W=D,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,B+1=V,E=X,0>=B,E>=1,A>=B] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[34]: 1
  with precondition: [E=0,F=1,S=0,X=0,Y=1,B+1=C,W=D,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,B+1=V,0>=B,A>=B] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[30],31]: 1+it1*(1)
  Such that:it1=<1*A,it1=<1*B,it1=<1*T,it1=<1*U,it1=<1*C+ -1,it1=<1*V+ -1,it1=<1*V+ -1*F,it1=<1*A+ -1*F+1,it1=<1*T+ -1*F+1
  with precondition: [S=0,Y=1,V=B+1,V=C,A=T,V=U+1,G=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,0>=X+1,F>=1,V>=F+1,A+1>=V] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[30],32]: 0+it1*(1)
  Such that:it1=<1*A,it1=<1*B,it1=<1*T,it1=<1*U,it1=<1*C+ -1,it1=<1*V+ -1,it1=<1*Y+ -1,it1=<1*Y+ -1*F,it1=<1*A+ -1*F+1,it1=<1*T+ -1*F+1,it1=<1*U+ -1*F+1
  with precondition: [S=1,B+1=C,A=T,B=U,B+1=V,G=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,F>=1,A>=B,Y>=F+1,B+1>=Y] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[30],33]: 1+it1*(1)
  Such that:it1=<1*A,it1=<1*B,it1=<1*T,it1=<1*U,it1=<1*C+ -1,it1=<1*V+ -1,it1=<1*V+ -1*F,it1=<1*A+ -1*F+1,it1=<1*T+ -1*F+1
  with precondition: [S=0,Y=1,V=B+1,V=C,A=T,V=U+1,G=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,F>=1,X>=1,V>=F+1,A+1>=V] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[30],34]: 1+it1*(1)
  Such that:it1=<1*A,it1=<1*B,it1=<1*T,it1=<1*U,it1=<1*C+ -1,it1=<1*V+ -1,it1=<1*V+ -1*F,it1=<1*A+ -1*F+1,it1=<1*T+ -1*F+1
  with precondition: [S=0,X=0,Y=1,B+1=C,A=T,B=U,B+1=V,G=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,F>=1,A>=B,B>=F] 

Inferred cost of f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1): 
f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[38]: 1
  with precondition: [S=0,Y=1,W=D,X=E,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,C=V,F>=B+1,A>=C+1] 

f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[40]: 1
  with precondition: [S=0,Y=1,W=D,X=E,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,C=V,C>=A+1,F>=B+1] 

f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[36],38]: 1+it1*(1)
  Such that:it1=<1*B+ -1*F+1,it1=<1*U+ -1*F+1
  with precondition: [S=0,Y=1,V=C,A=T,B=U,D=W,E=X,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,B>=F,A>=V+1] 

f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[36],40]: 1+it1*(1)
  Such that:it1=<1*B+ -1*F+1,it1=<1*U+ -1*F+1
  with precondition: [S=0,Y=1,V=C,A=T,B=U,D=W,E=X,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,V>=A+1,B>=F] 

Inferred cost of f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1): 
f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[43]: 1
  with precondition: [S=0,Y=1,T=A,V=C,W=D,X=E,Z=G,A1=H,B1=I,E1=L,F1=M,G1=N,H1=O,I1=P,B=U,B=D1,F>=B+1] 

f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[42],43]: 1+it1*(1)
  Such that:it1=<1*B+ -1*F+1,it1=<1*U+ -1*F+1
  with precondition: [S=0,Y=1,A=T,B=U,C=V,D=W,E=X,B=D1,L=E1,M=F1,N=G1,O=H1,P=I1,B>=F] 

Inferred cost of f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1): 
f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[46]: 1
  with precondition: [S=0,T=A,U=B+1,V=C,W=D,X=E,Z=G,A1=H,B1=I,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,F=Y,J=C1,F>=J+1] 

f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[45],46]: 1+it1*(1)
  Such that:it1=<1*Y+ -1*F
  with precondition: [S=0,A=T,B+1=U,C=V,D=W,E=X,J+1=Y,G=Z,H=A1,I=B1,J=C1,I1=D1+1,Q=J1,R=K1,J>=F,K>=I1] 

Inferred cost of f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1): 
f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[72]: 1
  with precondition: [B=1,S=1,A>=1] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[73]: 1+it1*(1)
  Such that:it1=<1,it1=<1*A
  with precondition: [B=1,S=1,A>=1] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[74]: 1
  with precondition: [B=1,S=1,U=1,V=C,W=D,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,0>=A] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[60,61,64,65,68,69],72]: 1+it1*(5+it2*(1)+it3*(1)+it4*(1))+it5*(5+it6*(1)+it7*(1)+it8*(1)+it9*(1))
  Such that:it1+it5=<-1*B+1*A+ -1,it1+it5=<1*A+ -1*B+ -1
            it4=<1*A+ -2,it3=<1*A+ -2,it2=<1*A+ -2,it2=<1*A
            it8=<1*A+ -2,it7=<1*A+ -2,it6=<1*A+ -2,it6=<1*A
  with precondition: [S=1,B>=1,A>=B+2] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[60,61,64,65,68,69],73]: 1+it1*(1)+it2*(5+it3*(1)+it4*(1)+it5*(1))+it6*(5+it7*(1)+it8*(1)+it9*(1)+it10*(1))
  Such that:it1=<1*A,it1=<1*A+ -1,it2+it6=<-1*B+1*A+ -1,it2+it6=<1*A+ -1*B+ -1
            it5=<1*A+ -2,it4=<1*A+ -2,it3=<1*A+ -2,it3=<1*A
            it9=<1*A+ -2,it8=<1*A+ -2,it7=<1*A+ -2,it7=<1*A
  with precondition: [S=1,B>=1,A>=B+2] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[62,74]: 6+it1*(1)+it2*(1)+it3*(1)
  Such that:it1=<1,it2=<1,it3=<1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,Y=1,D1=1,L=E1,M=F1,N=G1,O=H1,P=I1,0>=X+1,0>=C1] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[63,74]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1,it2=<1,it3=<1,it4=<1*C1,it4=<1*Y+ -1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,Y=C1+1,D1+1=I1,0>=X+1,0>=D1,Y>=2] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[66,74]: 6+it1*(1)+it2*(1)+it3*(1)
  Such that:it1=<1,it2=<1,it3=<1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,Y=1,D1=1,L=E1,M=F1,N=G1,O=H1,P=I1,0>=C1,X>=1] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[67,74]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1,it2=<1,it3=<1,it4=<1*C1,it4=<1*Y+ -1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,Y=C1+1,D1+1=I1,0>=D1,X>=1,Y>=2] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[70,74]: 6+it1*(1)+it2*(1)+it3*(1)
  Such that:it1=<1,it2=<1,it3=<1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,X=0,Y=1,D1=1,L=E1,M=F1,N=G1,O=H1,P=I1,0>=C1] 

f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[71,74]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1,it2=<1,it3=<1,it4=<1*C1,it4=<1*Y+ -1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,X=0,Y=C1+1,D1+1=I1,0>=D1,Y>=2] 

Inferred cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[76]: 1
  with precondition: [A=1] 

f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[77]: 2
  with precondition: [0>=A] 

f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[78]: 2
  with precondition: [A>=2] 

f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[79]: 2+it1*(1)
  Such that:it1=<1,it1=<1*A
  with precondition: [A>=2] 

f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[80]: 2+it1*(5+it2*(1)+it3*(1)+it4*(1))+it5*(5+it6*(1)+it7*(1)+it8*(1)+it9*(1))
  Such that:it1+it5=<1*A+ -2
            it4=<1*A+ -2,it3=<1*A+ -2,it2=<1*A+ -2,it2=<1*A
            it8=<1*A+ -2,it7=<1*A+ -2,it6=<1*A+ -2,it6=<1*A
  with precondition: [A>=3] 

f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[81]: 2+it1*(1)+it2*(5+it3*(1)+it4*(1)+it5*(1))+it6*(5+it7*(1)+it8*(1)+it9*(1)+it10*(1))
  Such that:it1=<1*A,it1=<1*A+ -1,it2+it6=<1*A+ -2
            it5=<1*A+ -2,it4=<1*A+ -2,it3=<1*A+ -2,it3=<1*A
            it9=<1*A+ -2,it8=<1*A+ -2,it7=<1*A+ -2,it7=<1*A
  with precondition: [A>=3] 

Solved cost expressions of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[76]: 1  with precondition: [A=1] 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[77]: 2  with precondition: [0>=A] 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[78]: 2  with precondition: [A>=2] 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[79]: 3  with precondition: [A>=2] 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[80]: inf  with precondition: [A>=3] 
f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[81]: inf  with precondition: [A>=3] 
Maximum cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 178 ms.
Invariants computed in 585 ms.
----Backward Invariants 261 ms.
----Transitive Invariants 100 ms.
Refinement performed in 2661 ms.
Termination proved in 258 ms.
Upper bounds computed in 7277 ms.
----Phase cost structures 7006 ms.
--------Equation cost structures 6957 ms.
--------Inductive compression(1) 1 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 249 ms.
----Solving cost expressions 3 ms.

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