warning: Ignored call to f0/49 in equation f17/49 warning: Ignored call to f0/49 in equation f9/49 warning: Ignored call to f0/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation f9/49 warning: Ignored call to loop_cont_f10/49 in equation loop_cont_f13/49 Warning: the following predicates are never called:[f9/49] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3): 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[41]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=C+1,0>=J2+1,0>=S3+1,P1>=0,H2>=2,Q3>=2] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[42]: 0 with precondition: [B=2,X1=1,Z1=2,B2=D,C=E,D2=F,E2=G,F2=H,G2=I,A=J,I2=K,J2=L,K2=M,L2=N,M2=O,N2=P,O2=Q,P2=R,Q2=S,R2=T,S2=U,T2=V,U2=W,V2=X,W2=Y,X2=Z,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,N3=P1,O3=Q1,P3=R1,Q3=S1,R3=T1,S3=U1,T3=V1,U3=W1,A=Y1,C=A2,C=C2,A=H2,C=L3,A>=2] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[43]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=C+1,0>=S3+1,P1>=0,H2>=2,J2>=1,Q3>=2] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[44]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=J2+1,0>=S3+1,C>=1,P1>=0,H2>=2,Q3>=2] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[45]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=S3+1,C>=1,P1>=0,H2>=2,J2>=1,Q3>=2] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[46]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=C+1,0>=J2+1,P1>=0,H2>=2,Q3>=2,S3>=1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[47]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=C+1,P1>=0,H2>=2,J2>=1,Q3>=2,S3>=1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[48]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,0>=J2+1,C>=1,P1>=0,H2>=2,Q3>=2,S3>=1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[49]: 1 with precondition: [A=2,B=2,J=2,X1=0,N2=0,U2=0,C=E,D2=F,E2=G,F2=H,G2=I,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,C=N1,M3=O1,T3=V1,U3=W1,J2=K2,C=X2,P1=N3,C>=1,P1>=0,H2>=2,J2>=1,Q3>=2,S3>=1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],41]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,N3=P1,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,V1=T3,W1=U3,0>=J2+1,0>=X2+1,0>=S3+1,B>=2,H2>=2,N3>=0,Q3>=2,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],42]: 0+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*Y1+ -2,it1=<1*Z1+ -2,it1=<1*E2+ -1,it1=<1*H2+ -2,it1=<1*E2+ -1*B+1 with precondition: [X1=1,C=E,A=J,A=Y1,E2+1=Z1,A2=C2,H=F2,I=G2,A=H2,K=I2,L=J2,M=K2,N=L2,O=M2,P=N2,Q=O2,R=P2,S=Q2,T=R2,U=S2,V=T2,W=U2,X=V2,Y=W2,Z=X2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,N1=L3,O1=M3,P1=N3,Q1=O3,R1=P3,S1=Q3,T1=R3,U1=S3,V1=T3,W1=U3,B>=2,E2>=B,A>=E2+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],43]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,N3=P1,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,V1=T3,W1=U3,0>=X2+1,0>=S3+1,B>=2,H2>=2,J2>=1,N3>=0,Q3>=2,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],44]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,P1=N3,V1=T3,W1=U3,0>=J2+1,0>=S3+1,B>=2,P1>=0,H2>=2,X2>=1,Q3>=2,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],45]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,N3=P1,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,V1=T3,W1=U3,0>=S3+1,B>=2,H2>=2,J2>=1,X2>=1,N3>=0,Q3>=2,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],46]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,N3=P1,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,V1=T3,W1=U3,0>=J2+1,0>=X2+1,B>=2,H2>=2,N3>=0,Q3>=2,S3>=1,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],47]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,N3=P1,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,V1=T3,W1=U3,0>=X2+1,B>=2,H2>=2,J2>=1,N3>=0,Q3>=2,S3>=1,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],48]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,P1=N3,V1=T3,W1=U3,0>=J2+1,B>=2,P1>=0,H2>=2,X2>=1,Q3>=2,S3>=1,A>=B+1] 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,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[40],49]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*J+ -2,it1=<1*J+ -1*B,it1=<1*E2+ -1 with precondition: [X1=0,N2=0,U2=0,C=E,A=J,N3=P1,A=E2+1,H=F2,I=G2,J2=K2,X=V2,Y=W2,A1=Y2,B1=Z2,C1=A3,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,O1=M3,V1=T3,W1=U3,B>=2,H2>=2,J2>=1,X2>=1,N3>=0,Q3>=2,S3>=1,A>=B+1] 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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3): 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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[55]: 0 with precondition: [X1=1,Y1=A,Z1=B,A2=C,B2=D,C2=E,D2=F,E2=G,F2=H,G2=I,H2=J,I2=K,J2=L,K2=M,L2=N,M2=O,N2=P,O2=Q,P2=R,Q2=S,R2=T,S2=U,T2=V,U2=W,V2=X,W2=Y,X2=Z,Y2=A1,Z2=B1,A3=C1,B3=D1,C3=E1,D3=F1,E3=G1,F3=H1,G3=I1,H3=J1,I3=K1,J3=L1,K3=M1,L3=N1,M3=O1,N3=P1,O3=Q1,P3=R1,Q3=S1,R3=T1,S3=U1,T3=V1,U3=W1] 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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[56]: 1 with precondition: [Z=0,X1=0,D3=0,F3=0,Y1=A,Z1=B,A2=C,B2=D,C2=E,D2=F,E2=G,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,J3=L1,K3=M1,L3=N1,M3=O1,N3=P1,O3=Q1,Q3=S1,R3=T1,S3=U1,K1+1=F2,I=G2,L=J2,L=B3,K1=C3,L=E3,L=G3,L=H3,K1=I3,H>=0,I>=0,L>=1,H2>=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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[57]: 1 with precondition: [Z=0,X1=0,D3=0,F3=0,Y1=A,Z1=B,A2=C,B2=D,C2=E,D2=F,E2=G,V2=X,W2=Y,Y2=A1,Z2=B1,A3=C1,J3=L1,K3=M1,L3=N1,M3=O1,N3=P1,O3=Q1,Q3=S1,R3=T1,S3=U1,K1+1=F2,I=G2,L=J2,L=B3,K1=C3,L=E3,L=G3,L=H3,K1=I3,0>=L+1,H>=0,I>=0,H2>=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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[51,52,53,54],55]: 0+it1*(1) Such that:it1=<1*I+1,it1=<1*I+ -1*G2 with precondition: [X1=1,N2=0,U2=0,A=Y1,B=Z1,C=A2,D=B2,E=C2,F=D2,G=E2,J2=K2,Z=W2,Z=X2,F2=Z2,D1=B3,E1=C3,F1=D3,G1=E3,H1=F3,I1=G3,J1=H3,K1=I3,L1=J3,M1=K3,N1=L3,O1=M3,P1=N3,Q1=O3,R1=P3,S1=Q3,T1=R3,U1=S3,V1=T3,W1=U3,F2+G2=H+I,A3+F2=H+I,H>=0,H2>=2,F2>=H+1,H+I+1>=F2] 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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[51,52,53,54],56]: 1+it1*(1) Such that:it1=<1*I+1,it1=<1*I+ -1*G2 with precondition: [Z=0,X1=0,W2=0,D3=0,F3=0,A=Y1,B=Z1,C=A2,D=B2,E=C2,F=D2,G=E2,K1+1=F2,E3=J2,E3=B3,K1=C3,E3=G3,E3=H3,K1=I3,L1=J3,M1=K3,N1=L3,O1=M3,P1=N3,Q1=O3,S1=Q3,T1=R3,U1=S3,H+I=G2+Z2,H+I=A3+Z2,H>=0,H2>=2,E3>=1,Z2>=H+1,H+I>=Z2] 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,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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[51,52,53,54],57]: 1+it1*(1) Such that:it1=<1*I+1,it1=<1*I+ -1*G2 with precondition: [Z=0,X1=0,W2=0,D3=0,F3=0,A=Y1,B=Z1,C=A2,D=B2,E=C2,F=D2,G=E2,K1+1=F2,E3=J2,E3=B3,K1=C3,E3=G3,E3=H3,K1=I3,L1=J3,M1=K3,N1=L3,O1=M3,P1=N3,Q1=O3,S1=Q3,T1=R3,U1=S3,H+I=G2+Z2,H+I=A3+Z2,0>=E3+1,H>=0,H2>=2,Z2>=H+1,H+I>=Z2] Inferred cost of f10(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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3): f10(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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[67]: 1 with precondition: [X1=1,Y1=A,Z1=B,A2=C,B2=D,C2=E,D2=F,E2=G,F2=H,G2=I,J2=L,K2=M,L2=N,M2=O,N2=P,O2=Q,P2=R,Q2=S,R2=T,S2=U,T2=V,U2=W,V2=X,W2=Y,X2=Z,Y2=A1,Z2=B1,A3=C1,F1=D1,C3=E1,J3=L1,K3=M1,L3=N1,M3=O1,N3=P1,O3=Q1,P3=R1,Q3=S1,R3=T1,S3=U1,T3=V1,U3=W1,K1=I3,K1>=0,H2>=2] f10(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,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3):[[59,60,61,62,63,64,65,66],67]: 1+it1*(1) Such that:it1=<1*K1+1,it1=<1*K1+ -1*I3 with precondition: [D1=0,F1=0,X1=1,A=Y1,B=Z1,C=A2,D=B2,E=C2,F=D2,G=E2,H=F2,I=G2,M=K2,N=L2,O=M2,P=N2,Q=O2,R=P2,S=Q2,T=R2,U=S2,V=T2,W=U2,Y=W2,Z=X2,A1=Y2,B1=Z2,C1=A3,E1=C3,I3=J3,M1=K3,N1=L3,O1=M3,P1=N3,Q1=O3,R1=P3,S1=Q3,T1=R3,U1=S3,V1=T3,W1=U3,H2>=2,I3>=0,K1>=I3+1] Inferred cost of loop_cont_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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): loop_cont_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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[69]: 1 with precondition: [F1=D1,K1>=0] loop_cont_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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[70]: 1+it1*(1) Such that:it1=<1*K1,it1=<1*K1+1 with precondition: [D1=0,F1=0,K1>=1] 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,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): 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,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]: 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,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]: 0+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[75]: 1 with precondition: [] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[76]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[77]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[78]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[79]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[80]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[81]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[82]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[83]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[84]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[85]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[86]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[87]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[88]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[89]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[90]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[91]: 2+it1*(1) Such that:it1=<1*I+1 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[92]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[93]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[94]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[95]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[96]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[97]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[98]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[99]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[100]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[101]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[102]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[103]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[104]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[105]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[106]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[107]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[108]: 1 with precondition: [] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[109]: inf with precondition: [] Solved cost expressions 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[75]: 1 with precondition: [] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[76]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[77]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[78]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[79]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[80]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[81]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[82]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[83]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[84]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[85]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[86]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[87]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[88]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[89]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[90]: 2 with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[91]: 1*I+3 with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[92]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[93]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[94]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[95]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[96]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[97]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[98]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[99]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[100]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[101]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[102]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[103]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[104]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[105]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[106]: inf with precondition: [P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[107]: inf with precondition: [H>=0,I>=0,P1>=0] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[108]: 1 with precondition: [] 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[109]: inf with precondition: [] Maximum 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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 497 ms. Invariants computed in 2501 ms. ----Backward Invariants 1283 ms. ----Transitive Invariants 457 ms. Refinement performed in 4336 ms. Termination proved in 1772 ms. Upper bounds computed in 1149 ms. ----Phase cost structures 418 ms. --------Equation cost structures 407 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 689 ms. ----Solving cost expressions 2 ms. Compressed phase information: 12 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 12038 ms.