warning: Ignored call to f65/24 in equation f63/24 warning: Ignored call to loop_cont_f61/24 in equation loop_cont_f36/24 warning: Ignored call to loop_cont_f31/24 in equation loop_cont_f15/24 Warning: the following predicates are never called:[f33/24,f63/24] Inferred cost of f15(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): f15(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[47]: 1 with precondition: [C=0,G=0,Q=0,X=1,Y=0,B1=0,F1=0,P1=0,W1=1,Z=A,A1=B,C1=D,D1=E,E1=F,G1=H,H1=I,I1=J,J1=K,K1=L,L1=M,M1=N,N1=O,O1=P,R1=S,S1=T,T1=U,U1=V,V1=W,R=Q1,0>=R] f15(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[42,43,44,45,46],47]: 1+it1*(2)+it2*(1) Such that:it1+it2=<1*R,it1+it2=<1*B1,it1+it2=<1*Q1,it1+it2=<1*Q1+ -1*C with precondition: [G=0,Q=0,X=1,Y=0,F1=0,P1=0,W1=1,A=Z,B=A1,R=B1,H=G1,I=H1,J=I1,K=J1,L=K1,M=L1,N=M1,O=N1,P=O1,R=Q1,T1=U1,T1=V1,C>=0,R>=C+1] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[51]: 2 with precondition: [Y=0,C1=D,D1=E,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,B=A1,C+1=B1,H=G1,M=K1,M=L1,M=M1,0>=M+1,A>=B+1,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[52]: 2 with precondition: [Y=0,D1=0,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,B=A1,C+1=B1,H=G1,M=K1,M=L1,M=M1,0>=M+1,B>=A,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[53]: 1 with precondition: [Y=1,C1=D,D1=E,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,B=A1,C=B1,H=G1,M=K1,M=L1,M=M1,0>=M+1,A>=B+1,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[54]: 2 with precondition: [Y=0,C1=D,D1=E,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,B=A1,C+1=B1,H=G1,M=K1,M=L1,M=M1,M>=1,A>=B+1,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[55]: 2 with precondition: [Y=0,D1=0,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,B=A1,C+1=B1,H=G1,M=K1,M=L1,M=M1,M>=1,B>=A,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[56]: 1 with precondition: [Y=1,C1=D,D1=E,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,B=A1,C=B1,H=G1,M=K1,M=L1,M=M1,M>=1,A>=B+1,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[57]: 1 with precondition: [L=0,M=0,Y=0,K1=0,L1=0,M1=0,Z=A,A1=B,C1=D,D1=E,E1=F,F1=G,H1=I,I1=J,J1=K,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,C+1=B1,H=G1,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[58]: 0 with precondition: [Y=1,Z=A,A1=B,C1=D,D1=E,E1=F,F1=G,H1=I,I1=J,J1=K,M=L,M1=N,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,C=B1,H=G1,M=K1,M=L1,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[49,50],52]: inf with precondition: [Y=0,D1=0,L=M,A=Z,B=A1,C+1=B1,F=E1,G=F1,H=G1,I=H1,L1=K1,L1=M1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1,0>=L1+1,B>=A,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[49,50],55]: inf with precondition: [Y=0,D1=0,L=M,A=Z,B=A1,C+1=B1,F=E1,G=F1,H=G1,I=H1,K1=L1,K1=M1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1,K1>=1,B>=A,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[49,50],57]: inf with precondition: [Y=0,K1=0,L1=0,M1=0,L=M,A=Z,B=A1,C+1=B1,D=C1,E=D1,F=E1,G=F1,H=G1,I=H1,O=N1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1,B>=A,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[49,50],58]: inf with precondition: [Y=1,L=M,A=Z,B=A1,C=B1,D=C1,E=D1,F=E1,G=F1,H=G1,I=H1,K1=L1,O=N1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1,B>=A,H>=C] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[49,50],59]...: inf with precondition: [L=M,1>=Y,Y>=0,B>=A,H>=C] Inferred cost of f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[68]: 2 with precondition: [C=1,G=0,Q=0,Y=1,H>=1,A>=B+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[69]: 2 with precondition: [C=1,G=0,Q=0,Y=1,H>=1,A>=B+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[70]: 1 with precondition: [C=1,G=0,Q=0,Y=1,H>=1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[71]: inf with precondition: [C=1,G=0,Q=0,Y=1,H>=1,B>=A] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[72]: 1 with precondition: [C=1,G=0,Q=0,Y=0,B1=1,F1=0,P1=0,Z=A,A1=B,C1=D,D1=E,E1=F,H1=I,I1=J,J1=K,K1=L,L1=M,M1=N,N1=O,O1=P,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,H=G1,0>=H] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[73]...: inf with precondition: [C=1,G=0,Q=0,1>=Y,H>=1,Y>=0,B>=A] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[74]...: inf with precondition: [C=1,G=0,Q=0,Y=1,H>=1,B>=A] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],68]: 2+it1*(3)+it2*(2)+it3*(inf) Such that:it1+it2+it3=<1*H,it1+it2+it3=<-1*C+1*H,it1+it2+it3=<1*H+ -1,it1+it2+it3=<1*H+ -1*C+1 with precondition: [G=0,Q=0,Y=1,C>=1,A>=B+1,H>=C+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],69]: 2+it1*(3)+it2*(2)+it3*(inf) Such that:it1+it2+it3=<1*H,it1+it2+it3=<-1*C+1*H,it1+it2+it3=<1*H+ -1,it1+it2+it3=<1*H+ -1*C+1 with precondition: [G=0,Q=0,Y=1,C>=1,A>=B+1,H>=C+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],70]: 1+it1*(3)+it2*(2)+it3*(inf) Such that:it1+it2+it3=<1*H,it1+it2+it3=<-1*C+1*H,it1+it2+it3=<1*H+ -1,it1+it2+it3=<1*H+ -1*C+1 with precondition: [G=0,Q=0,Y=1,C>=1,H>=C+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],71]: inf with precondition: [G=0,Q=0,Y=1,C>=1,B>=A,H>=C+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],72]: 1+it1*(3)+it2*(2)+it3*(inf) Such that:it1+it2+it3=<1*H,it1+it2+it3=<1*G1,it1+it2+it3=<1*B1+ -1,it1+it2+it3=<1*G1+ -1*C+1 with precondition: [G=0,Q=0,Y=0,F1=0,P1=0,A=Z,B=A1,H+1=B1,F=E1,H=G1,K1=L1,K1=M1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1,C>=1,H>=C] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],73]...: inf with precondition: [G=0,Q=0,1>=Y,C>=1,Y>=0,B>=A,H>=C+1] f36(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[60,61,62,63,64,65,66,67],74]...: inf with precondition: [G=0,Q=0,Y=1,C>=1,B>=A,H>=C+1] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[77]: 0 with precondition: [Y=1,Z=A,A1=B,B1=C,C1=D,D1=E,E1=F,F1=G,G1=H,H1=I,I1=J,J1=K,K1=L,L1=M,M1=N,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[76],77]: inf with precondition: [Y=1,A=Z,B=A1,C=B1,D=C1,E=D1,F=E1,G=F1,H=G1,I=H1,J=I1,K=J1,L=K1,M=L1,N=M1,O=N1,P=O1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[76],78]...: inf with precondition: [1>=Y,Y>=0] Inferred cost of loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[79]: 0 with precondition: [] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[80]: inf with precondition: [] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[81]...: inf with precondition: [] loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[82]...: inf with precondition: [] Inferred cost of f61(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): f61(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[85]: 0 with precondition: [Y=1,Z=A,A1=B,B1=C,C1=D,D1=E,E1=F,F1=G,G1=H,H1=I,I1=J,J1=K,K1=L,L1=M,M1=N,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X] f61(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[84],85]: inf with precondition: [Y=1,A=Z,B=A1,C=B1,D=C1,E=D1,F=E1,G=F1,H=G1,I=H1,J=I1,K=J1,L=K1,M=L1,N=M1,O=N1,P=O1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1] f61(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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[84],86]...: inf with precondition: [1>=Y,Y>=0] Inferred cost of loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[87]: 0 with precondition: [] loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[88]: inf with precondition: [] loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[89]...: inf with precondition: [] loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[90]...: inf with precondition: [] Inferred cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[92]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[93]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[94]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[95]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[96]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[97]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[98]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[99]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[100]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[101]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[102]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[103]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[104]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[105]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[106]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[107]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[108]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[109]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[110]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[111]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[112]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[113]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[114]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[115]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[116]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[117]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[118]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[119]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[120]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[121]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[122]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[123]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[124]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[125]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[126]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[127]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[128]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[129]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[130]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[131]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[132]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[133]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[134]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[135]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[136]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[137]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[138]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[139]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[140]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[141]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[142]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[143]...: inf with precondition: [] Solved cost expressions of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[92]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[93]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[94]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[95]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[96]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[97]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[98]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[99]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[100]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[101]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[102]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[103]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[104]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[105]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[106]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[107]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[108]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[109]: 3 with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[110]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[111]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[112]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[113]: inf with precondition: [A>=B+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[114]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[115]: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[116]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[117]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[118]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[119]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[120]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[121]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[122]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[123]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[124]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[125]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[126]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[127]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[128]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[129]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[130]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[131]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[132]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[133]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[134]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[135]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[136]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[137]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[138]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[139]...: inf with precondition: [B>=A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[140]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[141]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[142]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[143]...: inf with precondition: [] Maximum cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 283 ms. Invariants computed in 1293 ms. ----Backward Invariants 817 ms. ----Transitive Invariants 168 ms. Refinement performed in 1249 ms. Termination proved in 472 ms. Upper bounds computed in 509 ms. ----Phase cost structures 219 ms. --------Equation cost structures 207 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 263 ms. ----Solving cost expressions 0 ms. Compressed phase information: 14 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 4218 ms.