warning: Ignored call to f1/34 in equation f0/34 warning: Ignored call to loop_cont_f5/34 in equation f0/34 warning: Ignored call to loop_cont_f5/34 in equation f0/34 warning: Ignored call to loop_cont_f2/34 in equation loop_cont_f11/34 Inferred cost of f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2): f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[26]: 1 with precondition: [A=2,B=2,K=2,I1=0,C=E,O1=F,P1=G,Q1=H,R1=I,Y1=P,Z1=Q,A2=R,B2=S,C2=T,D2=U,E2=V,C=W,G2=X,H2=Y,K2=B1,L2=C1,M2=D1,N2=E1,O2=F1,P2=G1,J=S1,W1=U1,J=V1,J=X1,H1=Q2,0>=J+1,H1>=2,T1>=2] f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[27]: 0 with precondition: [B=2,I1=1,K1=2,M1=D,C=E,O1=F,P1=G,Q1=H,R1=I,S1=J,A=K,U1=L,V1=M,W1=N,X1=O,Y1=P,Z1=Q,A2=R,B2=S,C2=T,D2=U,E2=V,C=W,G2=X,H2=Y,I2=Z,J2=A1,K2=B1,L2=C1,M2=D1,N2=E1,O2=F1,P2=G1,Q2=H1,A=J1,C=L1,C=N1,A=T1,C=F2,A>=2] f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[28]: 1 with precondition: [A=2,B=2,K=2,I1=0,C=E,O1=F,P1=G,Q1=H,R1=I,Y1=P,Z1=Q,A2=R,B2=S,C2=T,D2=U,E2=V,C=W,G2=X,H2=Y,K2=B1,L2=C1,M2=D1,N2=E1,O2=F1,P2=G1,J=S1,W1=U1,J=V1,J=X1,H1=Q2,J>=1,H1>=2,T1>=2] f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[25],26]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*K+ -2,it1=<1*K+ -1*B,it1=<1*P1+ -1 with precondition: [I1=0,C=E,A=K,Q2=H1,A=P1+1,I=Q1,I=R1,J=S1,J=V1,U1=W1,J=X1,P=Y1,Q=Z1,R=A2,S=B2,T=C2,U=D2,V=E2,X=G2,Y=H2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,0>=J+1,B>=2,T1>=2,Q2>=2,A>=B+1] f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[25],27]: 0+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*K+ -2,it1=<1*K+ -1*B,it1=<1*J1+ -2,it1=<1*K1+ -2,it1=<1*P1+ -1,it1=<1*T1+ -2,it1=<1*P1+ -1*B+1 with precondition: [I1=1,C=E,A=K,A=J1,P1+1=K1,L1=N1,I=Q1,I=R1,J=S1,A=T1,L=U1,M=V1,N=W1,O=X1,P=Y1,Q=Z1,R=A2,S=B2,T=C2,U=D2,V=E2,W=F2,X=G2,Y=H2,Z=I2,A1=J2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,H1=Q2,B>=2,P1>=B,A>=P1+1] f11(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[25],28]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*K+ -2,it1=<1*K+ -1*B,it1=<1*P1+ -1 with precondition: [I1=0,C=E,V1=J,A=K,Q2=H1,A=P1+1,I=Q1,I=R1,V1=S1,U1=W1,V1=X1,P=Y1,Q=Z1,R=A2,S=B2,T=C2,U=D2,V=E2,X=G2,Y=H2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,B>=2,T1>=2,V1>=1,Q2>=2,A>=B+1] Inferred cost of f5(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2): f5(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[32]: 0 with precondition: [K=1,I1=1,T1=1,J1=A,K1=B,L1=C,M1=D,N1=E,O1=F,P1=G,Q1=H,R1=I,N=L,J=M,J=O,Y1=P,Z1=Q,A2=R,B2=S,C2=T,D2=U,E2=V,F2=W,G2=X,H2=Y,I2=Z,J2=A1,K2=B1,L2=C1,M2=D1,N2=E1,O2=F1,P2=G1,Q2=H1,J=S1,N=U1,J=V1,N=W1,J=X1] f5(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[30],32]: inf with precondition: [K=1,I1=1,T1=1,J=M,L=N,J=O,A=J1,B=K1,C=L1,D=M1,E=N1,F=O1,G=P1,H=Q1,I=R1,J=S1,J=V1,U1=W1,J=X1,P=Y1,Q=Z1,R=A2,I=B2,U=C2,U=D2,V=E2,W=F2,X=G2,Y=H2,Z=I2,A1=J2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,H1=Q2,0>=J+1] f5(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[30],33]...: inf with precondition: [K=1,J=M,L=N,J=O,0>=J+1,1>=I1,I1>=0] f5(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[31],32]: inf with precondition: [K=1,I1=1,T1=1,J=M,L=N,J=O,A=J1,B=K1,C=L1,D=M1,E=N1,F=O1,G=P1,H=Q1,I=R1,J=S1,J=V1,U1=W1,J=X1,P=Y1,Q=Z1,R=A2,I=B2,U=C2,U=D2,V=E2,W=F2,X=G2,Y=H2,Z=I2,A1=J2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,H1=Q2,J>=1] f5(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[31],33]...: inf with precondition: [K=1,J=M,L=N,J=O,1>=I1,J>=1,I1>=0] Inferred cost of f2(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2): f2(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[36]: 0 with precondition: [I1=1,J1=A,K1=B,L1=C,M1=D,N1=E,O1=F,P1=G,Q1=H,R1=I,S1=J,T1=K,U1=L,V1=M,W1=N,X1=O,Y1=P,Z1=Q,A2=R,B2=S,C2=T,D2=U,E2=V,F2=W,G2=X,H2=Y,I2=Z,J2=A1,K2=B1,L2=C1,M2=D1,N2=E1,O2=F1,P2=G1,Q2=H1] f2(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[34],36]: inf with precondition: [I1=1,A=J1,B=K1,C=L1,D=M1,E=N1,F=O1,G=P1,H=Q1,I=R1,J=S1,J=V1,U1=W1,J=X1,Q=Y1,Q=Z1,I=A2,S=B2,T=C2,U=D2,V=E2,W=F2,X=G2,Y=H2,Z=I2,A1=J2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,H1=Q2,0>=J+1,T1>=2] f2(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[34],37]...: inf with precondition: [0>=J+1,1>=I1,I1>=0] f2(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[35],36]: inf with precondition: [I1=1,A=J1,B=K1,C=L1,D=M1,E=N1,F=O1,G=P1,H=Q1,I=R1,J=S1,J=V1,U1=W1,J=X1,Q=Y1,Q=Z1,I=A2,S=B2,T=C2,U=D2,V=E2,W=F2,X=G2,Y=H2,Z=I2,A1=J2,B1=K2,C1=L2,D1=M2,E1=N2,F1=O2,G1=P2,H1=Q2,J>=1,T1>=2] f2(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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2):[[35],37]...: inf with precondition: [1>=I1,J>=1,I1>=0] Inferred cost of loop_cont_f11(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): loop_cont_f11(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):[38]: 0 with precondition: [] loop_cont_f11(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):[39]: inf with precondition: [0>=J+1] loop_cont_f11(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):[40]: inf with precondition: [J>=1] loop_cont_f11(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):[41]...: inf with precondition: [0>=J+1] loop_cont_f11(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):[42]...: inf with precondition: [J>=1] loop_cont_f11(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):[43]...: inf with precondition: [0>=J+1] loop_cont_f11(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):[44]...: inf with precondition: [J>=1] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1): 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[46]: 1 with precondition: [Y=0] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[47]: 2 with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[48]: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[49]: 2 with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[50]: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[51]: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[52]: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[53]: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[54]: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[55]: 1 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[56]: 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[57]: 1 with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[58]: inf with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[59]: 1 with precondition: [J>=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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[60]: inf with precondition: [J>=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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[61]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[62]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[63]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[64]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[65]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[66]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[67]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[68]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[69]...: inf with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[70]...: inf with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[71]...: inf with precondition: [J>=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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[72]...: inf with precondition: [J>=1] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1): 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[46]: 1 with precondition: [Y=0] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[47]: 2 with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[48]: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[49]: 2 with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[50]: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[51]: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[52]: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[53]: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[54]: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[55]: 1 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[56]: 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[57]: 1 with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[58]: inf with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[59]: 1 with precondition: [J>=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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[60]: inf with precondition: [J>=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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[61]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[62]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[63]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[64]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[65]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[66]...: inf with precondition: [0>=J+1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[67]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[68]...: inf with precondition: [J>=1,H1>=2] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[69]...: inf with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[70]...: inf with precondition: [0>=J+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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[71]...: inf with precondition: [J>=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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1):[72]...: inf with precondition: [J>=1] 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 145 ms. Invariants computed in 833 ms. ----Backward Invariants 393 ms. ----Transitive Invariants 155 ms. Refinement performed in 834 ms. Termination proved in 464 ms. Upper bounds computed in 469 ms. ----Phase cost structures 149 ms. --------Equation cost structures 139 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 302 ms. ----Solving cost expressions 0 ms. Compressed phase information: 8 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 3109 ms.