WARNING: Excluded non-linear constraints:[P1=D+L1*M1,Q1=E+N1*O1]
WARNING: Excluded non-linear constraints:[R1=G+L1*M1,S1=H+N1*O1,T1=I+P1*Q1]
warning: Ignored call to f1/18 in equation f2/18 
warning: Ignored call to loop_cont_f13/18 in equation f2/18 
warning: Ignored call to loop_cont_f13/18 in equation f2/18 
Inferred cost of f20(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): 
f20(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]: 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] 

f20(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]: 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] 

f20(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: [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] 

f20(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):[35]: 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] 

f20(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],32]: 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] 

f20(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],33]: 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] 

f20(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],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,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] 

f20(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],35]: 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 f31(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): 
f31(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):[39]: 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] 

f31(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):[41]: 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] 

f31(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):[[37],39]: 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] 

f31(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):[[37],41]: 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 f45(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): 
f45(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):[44]: 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,B+1>=2*C1,F>=B+1,3*C1>=B+2] 

f45(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],44]: 1+it1*(1)
  Such that:it1=<1*B+ -1*F+1,it1=<1*U+ -1*F+1
  with precondition: [S=0,Y=1,D1=B,A=T,D1=U,C=V,D=W,E=X,L=E1,M=F1,N=G1,O=H1,P=I1,D1+1>=2*C1,D1>=F,3*C1>=D1+2] 

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):[48]: 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):[[47],48]: 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 f13(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): 
f13(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):[56]: 1
  with precondition: [B=1,S=1,A>=1] 

f13(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):[57]: 1+it1*(1)
  Such that:it1=<1,it1=<1*A
  with precondition: [B=1,S=1,A>=1] 

f13(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):[58]: 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] 

f13(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):[[50,52,54],56]: 1+it1*(5+it2*(1)+it3*(1)+it4*(1)+it5*(1))
  Such that:it1=<-1*B+1*A+ -1,it1=<1*A+ -1*B+ -1
            it5=<1/2*A+ -1/2,it4=<3/2*A+ -7/2,it4=<1*A+ -2,it3=<3/2*A+ -7/2,it3=<1*A+ -2,it2=<3/2*A+ -7/2,it2=<1*A+ -2,it2=<1*A
  with precondition: [S=1,B>=1,A>=B+2] 

f13(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):[[50,52,54],57]: 1+it1*(1)+it2*(5+it3*(1)+it4*(1)+it5*(1)+it6*(1))
  Such that:it1=<1*A,it1=<1*A+ -1,it2=<-1*B+1*A+ -1,it2=<1*A+ -1*B+ -1
            it6=<1/2*A+ -1/2,it5=<3/2*A+ -7/2,it5=<1*A+ -2,it4=<3/2*A+ -7/2,it4=<1*A+ -2,it3=<3/2*A+ -7/2,it3=<1*A+ -2,it3=<1*A
  with precondition: [S=1,B>=1,A>=B+2] 

f13(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):[51,58]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1,it2=<1,it3=<1,it4=<1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,Y=2,C1=1,D1+1=I1,0>=X+1,0>=D1] 

f13(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):[53,58]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1,it2=<1,it3=<1,it4=<1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,Y=2,C1=1,D1+1=I1,0>=D1,X>=1] 

f13(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):[55,58]: 6+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1,it2=<1,it3=<1,it4=<1
  with precondition: [A=1,B=1,S=1,T=1,U=2,V=2,X=0,Y=2,C1=1,D1+1=I1,0>=D1] 

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

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

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

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

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

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

Solved cost expressions of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[60]: 1  with precondition: [A=1] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[61]: 2  with precondition: [0>=A] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[62]: 2  with precondition: [A>=2] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[63]: 3  with precondition: [A>=2] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[64]: (7/2*A+ -3/2)* (1*A+ -2)+2  with precondition: [A>=3] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[65]: 1*A+ -1+ (7/2*A+ -3/2)* (1*A+ -2)+2  with precondition: [A>=3] 
Maximum cost of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): max([3, (7/2*A+ -3/2)* (1*A+ -2)+2,1*A+ -1+ (7/2*A+ -3/2)* (1*A+ -2)+2]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 183 ms.
Invariants computed in 412 ms.
----Backward Invariants 212 ms.
----Transitive Invariants 62 ms.
Refinement performed in 1508 ms.
Termination proved in 156 ms.
Upper bounds computed in 5558 ms.
----Phase cost structures 5315 ms.
--------Equation cost structures 5275 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 225 ms.
----Solving cost expressions 4 ms.

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