warning: Ignored call to loop_cont_f540/42 in equation loop_cont_f526/42 Inferred cost of f422(A,B,C,D,E,F,G,H,I,J,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): f422(A,B,C,D,E,F,G,H,I,J,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):[[59],60]: 1+it1*(1) Such that:it1=<150,it1=<-1*E+150 with precondition: [A=3,B=43690,Q1=0,S1=43690,V1=150,W1=0,R1=T1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,R1=F3,R1=G3,149>=E,E>=0] Inferred cost of f441(A,B,C,D,E,F,G,H,I,J,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): f441(A,B,C,D,E,F,G,H,I,J,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):[[62],63]: 1+it1*(1) Such that:it1=<50,it1=<-1*H+50 with precondition: [Q1=0,Y1=50,A=R1,B=S1,C=T1,D=U1,E=V1,F+1=W1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,49>=F,49>=H,H>=0] Inferred cost of f437(A,B,C,D,E,F,G,H,I,J,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): f437(A,B,C,D,E,F,G,H,I,J,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):[66]: 1 with precondition: [Q1=0,Z1=0,R1=A,S1=B,T1=C,U1=D,V1=E,X1=G,Y1=H,A2=J,B2=K,C2=L,D2=M,E2=N,F2=O,G2=P,H2=Q,I2=R,J2=S,K2=T,L2=U,M2=V,N2=W,O2=X,P2=Y,Q2=Z,R2=A1,S2=B1,T2=C1,U2=D1,V2=E1,W2=F1,X2=G1,Y2=H1,Z2=I1,A3=J1,B3=K1,C3=L1,D3=M1,E3=N1,F3=O1,G3=P1,F=W1,F>=50] f437(A,B,C,D,E,F,G,H,I,J,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):[[65],66]: 1+it1*(2+it2*(1)) Such that:it1=<-1*F+50 it2=<50 with precondition: [Q1=0,W1=50,Y1=50,Z1=0,A=R1,B=S1,C=T1,D=U1,E=V1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,49>=F] Inferred cost of f461(A,B,C,D,E,F,G,H,I,J,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): f461(A,B,C,D,E,F,G,H,I,J,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):[[68],69]: 1+it1*(1) Such that:it1=<16,it1=<1/2*D2,it1=<-1/2*M+16,it1=<1/2*D2+ -1/2*M,it1=<33/2 with precondition: [Q1=0,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I+2=Z1,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,99>=I,33>=D2,M>=0,D2>=32,D2>=M+2] Inferred cost of f455(A,B,C,D,E,F,G,H,I,J,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): f455(A,B,C,D,E,F,G,H,I,J,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):[72]: 1 with precondition: [Q1=0,H2=98,E3=100,R1=A,S1=B,T1=C,U1=D,V1=E,W1=F,X1=G,Y1=H,A2=J,B2=K,C2=L,D2=M,E2=N,F2=O,G2=P,J2=S,K2=T,L2=U,M2=V,N2=W,O2=X,P2=Y,Q2=Z,R2=A1,S2=B1,T2=C1,U2=D1,V2=E1,W2=F1,X2=G1,Y2=H1,Z2=I1,A3=J1,B3=K1,C3=L1,D3=M1,F3=O1,G3=P1,I=Z1,I>=100] f455(A,B,C,D,E,F,G,H,I,J,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):[[71],72]: 1+it1*(2+it2*(1)) Such that:it1=<-1/2*I+50,it1=<1/2*Z1+ -1/2*I it2=<33/2,it2=<16 with precondition: [Q1=0,H2=98,E3=100,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,S=J2,T=K2,U=L2,V=M2,W=N2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,O1=F3,P1=G3,101>=Z1,33>=D2,Z1>=100,D2>=32,Z1>=I+2] Inferred cost of f485(A,B,C,D,E,F,G,H,I,J,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): f485(A,B,C,D,E,F,G,H,I,J,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):[75]: 1 with precondition: [Q1=0,J2=0,R1=A,T1=C,U1=D,V1=E,W1=F,X1=G,Y1=H,Z1=I,A2=J,B2=K,C2=L,D2=M,E2=N,F2=O,G2=P,L2=U,M2=V,N2=W,O2=X,P2=Y,Q2=Z,R2=A1,S2=B1,T2=C1,U2=D1,V2=E1,W2=F1,X2=G1,Y2=H1,Z2=I1,A3=J1,B3=K1,C3=L1,E3=N1,F3=O1,G3=P1,R=S1,Q=H2,R=I2,R=D3,0>=Q+1] f485(A,B,C,D,E,F,G,H,I,J,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):[[74],75]: 1+it1*(1) Such that:it1=<1*Q+1 with precondition: [Q1=0,H2+1=0,J2=0,A=R1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,S1=I2,U=L2,V=M2,W=N2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,S1=D3,N1=E3,O1=F3,P1=G3,Q>=0] Inferred cost of f501(A,B,C,D,E,F,G,H,I,J,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): f501(A,B,C,D,E,F,G,H,I,J,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):[78]: 1 with precondition: [Q1=0,M2=17,N2=2,Y2=1,B3=1,T1=C,U1=D,V1=E,W1=F,X1=G,Y1=H,Z1=I,A2=J,B2=K,C2=L,D2=M,E2=N,F2=O,G2=P,H2=Q,I2=R,K2=T,L2=U,O2=X,P2=Y,Q2=Z,R2=A1,S2=B1,T2=C1,U2=D1,W2=F1,D3=M1,E3=N1,F3=O1,G3=P1,A=R1,B=S1,S=J2,B=V2,B=X2,A=A3,S>=50] f501(A,B,C,D,E,F,G,H,I,J,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):[[77],78]: 1+it1*(1) Such that:it1=<-1*S+50 with precondition: [Q1=0,J2=50,M2=17,N2=2,Y2=1,B3=1,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,X=O2,Y=P2,Z=Q2,A1=R2,B1=S2,C1=T2,D1=U2,B=V2,F1=W2,B=X2,A=A3,M1=D3,N1=E3,O1=F3,P1=G3,49>=S] Inferred cost of f526(A,B,C,D,E,F,G,H,I,J,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): f526(A,B,C,D,E,F,G,H,I,J,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):[81]: 1 with precondition: [Q1=0,O2=1,R2=0,S2=13,T2=8,R1=A,S1=B,T1=C,U1=D,V1=E,W1=F,X1=G,Y1=H,Z1=I,A2=J,B2=K,C2=L,D2=M,E2=N,F2=O,G2=P,H2=Q,I2=R,J2=S,K2=T,L2=U,P2=Y,Q2=Z,X2=G1,Y2=H1,Z2=I1,A3=J1,B3=K1,C3=L1,D3=M1,E3=N1,F3=O1,G3=P1,V=M2,W=N2,E1=U2,E1=V2,E1=W2,W>=V+1] f526(A,B,C,D,E,F,G,H,I,J,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):[[80],81]: 1+it1*(1) Such that:it1=<1*V+ -1*W+1,it1=<1*M2+ -1*W+1 with precondition: [Q1=0,O2=1,R2=0,S2=13,T2=8,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,V+1=N2,Y=P2,Z=Q2,E1=U2,E1=V2,E1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,V>=W] Inferred cost of f546(A,B,C,D,E,F,G,H,I,J,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): f546(A,B,C,D,E,F,G,H,I,J,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):[[83],84]: 1+it1*(1) Such that:it1=<4,it1=<-1*Z+4 with precondition: [Q1=0,Q2=4,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,X=O2,Y+1=P2,A1=R2,B1=S2,C1=T2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,7>=Y,3>=Z,Z>=0] Inferred cost of f543(A,B,C,D,E,F,G,H,I,J,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): f543(A,B,C,D,E,F,G,H,I,J,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):[[86],87]: 1+it1*(2+it2*(1)) Such that:it1=<8,it1=<-1*Y+8 it2=<4 with precondition: [Q1=0,P2=8,Q2=4,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,X+7=O2,A1+3=R2,B1+3=S2,C1=T2+7,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,8>=X,7>=Y] Inferred cost of f540(A,B,C,D,E,F,G,H,I,J,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): f540(A,B,C,D,E,F,G,H,I,J,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):[90]: 1 with precondition: [Q1=1,R1=A,S1=B,T1=C,U1=D,V1=E,W1=F,X1=G,Y1=H,Z1=I,A2=J,B2=K,C2=L,D2=M,E2=N,F2=O,G2=P,H2=Q,I2=R,J2=S,K2=T,L2=U,M2=V,N2=W,P2=Y,Q2=Z,R2=A1,S2=B1,T2=C1,U2=D1,V2=E1,W2=F1,X2=G1,Y2=H1,Z2=I1,A3=J1,B3=K1,C3=L1,D3=M1,E3=N1,F3=O1,G3=P1,X=O2,X>=9] f540(A,B,C,D,E,F,G,H,I,J,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):[[89],90]: 1+it1*(2+it2*(2+it3*(1))) Such that:it1=<-1/7*X+9/7,it1=<1/7*O2+ -1/7*X it2=<8 it3=<4 with precondition: [Q1=1,P2=8,Q2=4,A=R1,B=S1,C=T1,D=U1,E=V1,F=W1,G=X1,H=Y1,I=Z1,J=A2,K=B2,L=C2,M=D2,N=E2,O=F2,P=G2,Q=H2,R=I2,S=J2,T=K2,U=L2,V=M2,W=N2,D1=U2,E1=V2,F1=W2,G1=X2,H1=Y2,I1=Z2,J1=A3,K1=B3,L1=C3,M1=D3,N1=E3,O1=F3,P1=G3,15>=O2,O2>=9,O2>=X+7,R2>=A1+3,S2>=B1+3,C1>=T2+7] Inferred cost of loop_cont_f526(A,B,C,D,E,F,G,H,I,J,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): loop_cont_f526(A,B,C,D,E,F,G,H,I,J,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):[92]: 1 with precondition: [X>=9] loop_cont_f526(A,B,C,D,E,F,G,H,I,J,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):[93]: 1+it1*(2+it2*(2+it3*(1))) Such that:it1=<-1/7*X+9/7,it1=<-1/7*X+15/7 it2=<8 it3=<4 with precondition: [8>=X] Inferred cost of loop_cont_f501(A,B,C,D,E,F,G,H,I,J,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): loop_cont_f501(A,B,C,D,E,F,G,H,I,J,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):[95]: 2+it1*(2+it2*(2+it3*(1))) Such that:it1=<2,it1=<8/7 it2=<8 it3=<4 with precondition: [W>=V+1] loop_cont_f501(A,B,C,D,E,F,G,H,I,J,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):[96]: 2+it1*(1)+it2*(2+it3*(2+it4*(1))) Such that:it1=<1*V+ -1*W+1,it2=<2,it2=<8/7 it3=<8 it4=<4 with precondition: [V>=W] Inferred cost of loop_cont_f485(A,B,C,D,E,F,G,H,I,J,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): loop_cont_f485(A,B,C,D,E,F,G,H,I,J,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):[98]: 3+it1*(1)+it2*(2+it3*(2+it4*(1))) Such that:it1=<16,it2=<2,it2=<8/7 it3=<8 it4=<4 with precondition: [S>=50] loop_cont_f485(A,B,C,D,E,F,G,H,I,J,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):[99]: 3+it1*(1)+it2*(1)+it3*(2+it4*(2+it5*(1))) Such that:it1=<-1*S+50,it2=<16,it3=<2,it3=<8/7 it4=<8 it5=<4 with precondition: [49>=S] Inferred cost of loop_cont_f455(A,B,C,D,E,F,G,H,I,J,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): loop_cont_f455(A,B,C,D,E,F,G,H,I,J,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):[101]: 4+it1*(1)+it2*(1)+it3*(2+it4*(2+it5*(1))) Such that:it1=<50,it2=<16,it3=<2,it3=<8/7 it4=<8 it5=<4 with precondition: [0>=Q+1] loop_cont_f455(A,B,C,D,E,F,G,H,I,J,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):[102]: 4+it1*(1)+it2*(1)+it3*(1)+it4*(2+it5*(2+it6*(1))) Such that:it1=<1*Q+1,it2=<50,it3=<16,it4=<2,it4=<8/7 it5=<8 it6=<4 with precondition: [Q>=0] Inferred cost of loop_cont_f437(A,B,C,D,E,F,G,H,I,J,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): loop_cont_f437(A,B,C,D,E,F,G,H,I,J,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):[104]: 5+it1*(1)+it2*(1)+it3*(1)+it4*(2+it5*(2+it6*(1))) Such that:it1=<99,it2=<50,it3=<16,it4=<2,it4=<8/7 it5=<8 it6=<4 with precondition: [I>=100] loop_cont_f437(A,B,C,D,E,F,G,H,I,J,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):[105]: 5+it1*(2+it2*(1))+it3*(1)+it4*(1)+it5*(1)+it6*(2+it7*(2+it8*(1))) Such that:it1=<-1/2*I+50,it1=<-1/2*I+101/2,it3=<99,it4=<50,it5=<16,it6=<2,it6=<8/7 it2=<33/2,it2=<16 it7=<8 it8=<4 with precondition: [99>=I] Inferred cost of loop_cont_f422(A,B,C,D,E,F,G,H,I,J,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): loop_cont_f422(A,B,C,D,E,F,G,H,I,J,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):[107]: 6+it1*(2+it2*(1))+it3*(1)+it4*(1)+it5*(1)+it6*(2+it7*(2+it8*(1))) Such that:it1=<50,it1=<101/2,it3=<99,it4=<50,it5=<16,it6=<2,it6=<8/7 it2=<33/2,it2=<16 it7=<8 it8=<4 with precondition: [F>=50] loop_cont_f422(A,B,C,D,E,F,G,H,I,J,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):[108]: 6+it1*(2+it2*(1))+it3*(2+it4*(1))+it5*(1)+it6*(1)+it7*(1)+it8*(2+it9*(2+it10*(1))) Such that:it1=<-1*F+50,it3=<50,it3=<101/2,it5=<99,it6=<50,it7=<16,it8=<2,it8=<8/7 it2=<50 it4=<33/2,it4=<16 it9=<8 it10=<4 with precondition: [49>=F] 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,I1,J1,K1,L1,M1,N1,O1,P1): 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,I1,J1,K1,L1,M1,N1,O1,P1):[110]: 8+it1*(1)+it2*(2+it3*(1))+it4*(2+it5*(1))+it6*(1)+it7*(1)+it8*(1)+it9*(2+it10*(2+it11*(1))) Such that:it1=<150,it2=<50,it4=<50,it4=<101/2,it6=<99,it7=<50,it8=<16,it9=<2,it9=<8/7 it3=<50 it5=<33/2,it5=<16 it10=<8 it11=<4 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1): 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,I1,J1,K1,L1,M1,N1,O1,P1):[110]: 27161/7 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1): 27161/7 Asymptotic class: constant Time statistics: Partial evaluation computed in 718 ms. Invariants computed in 2001 ms. ----Backward Invariants 660 ms. ----Transitive Invariants 512 ms. Refinement performed in 2145 ms. Termination proved in 1815 ms. Upper bounds computed in 713 ms. ----Phase cost structures 300 ms. --------Equation cost structures 287 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 384 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 9151 ms.