warning: Ignored call to f22/48 in equation f21/48 warning: Ignored call to f22/48 in equation f4/48 warning: Ignored call to f22/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f4/48 warning: Ignored call to loop_cont_f5/48 in equation f7/48 warning: Ignored call to loop_cont_f5/48 in equation f7/48 warning: Ignored call to loop_cont_f5/48 in equation f7/48 warning: Ignored call to loop_cont_f5/48 in equation loop_cont_f11/48 Warning: the following predicates are never called:[f16/48,f17/48,f4/48,f7/48] 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): 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):[46]: 1 with precondition: [A=2,B=2,E=0,F=2,W1=0,B2=0,J=C,J=I,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,D=X1,D=A2,J=I2,J=J2,J=K2,0>=J+1,C2>=2,D>=C2,L2>=C2] 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):[47]: 0 with precondition: [A=2,W1=1,X1=2,J=C,A2=D,B2=E,B=F,D2=G,E2=H,J=I,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,B=Y1,J=Z1,B=C2,J=F2,J=G2,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,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):[48]: 1 with precondition: [A=2,B=2,E=0,F=2,W1=0,B2=0,J=C,J=I,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,D=X1,D=A2,J=I2,J=J2,J=K2,J>=1,C2>=2,D>=C2,L2>=C2] 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):[[45],46]: 1+it1*(1) Such that:it1=<1*B+ -2,it1=<1*F+ -2,it1=<1*N2+ -1,it1=<1*N2+ -1*A+1 with precondition: [E=0,W1=0,B2=0,B=F,C=J,D=X1,D=A2,J2=I2,J2=K2,B=N2+1,R=O2,S=P2,T=Q2,U=R2,V=S2,W=T2,X=U2,Y=V2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,0>=J2+1,A>=2,C2>=2,B>=A+1,D>=C2,L2>=C2] 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):[[45],47]: 0+it1*(1) Such that:it1=<1*B+ -2,it1=<1*F+ -2,it1=<1*F+ -1*A,it1=<1*X1+ -2,it1=<1*Y1+ -2,it1=<1*C2+ -2,it1=<1*N2+ -1,it1=<1*N2+ -1*A+1 with precondition: [W1=1,B=F,C=J,B=Y1,D=A2,E=B2,B=C2,G=D2,H=E2,I=F2,Z1=G2,L=I2,M=J2,N=K2,O=L2,X1=N2+1,R=O2,S=P2,T=Q2,U=R2,V=S2,W=T2,X=U2,Y=V2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,A>=2,X1>=A+1,B>=X1] 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):[[45],48]: 1+it1*(1) Such that:it1=<1*B+ -2,it1=<1*F+ -2,it1=<1*N2+ -1,it1=<1*N2+ -1*A+1 with precondition: [E=0,W1=0,B2=0,B=F,C=J,D=X1,D=A2,K2=I2,K2=J2,B=N2+1,R=O2,S=P2,T=Q2,U=R2,V=S2,W=T2,X=U2,Y=V2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,A>=2,C2>=2,K2>=1,B>=A+1,D>=C2,L2>=C2] 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,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): 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,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):[54]: 1 with precondition: [N=0,Y=0,W1=0,V2=0,X1=A,Y1=B,Z1=C,D2=G,E2=H,F2=I,G2=J,H2=K,L2=O,M2=P,N2=Q,O2=R,P2=S,Q2=T,R2=U,S2=V,T2=W,E=X,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,D=A2,E=B2,L=I2,L=J2,L=K2,E=U2,0>=L+1,D>=0,E>=0,C2>=2] 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,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):[55]: 0 with precondition: [W1=1,X1=A,Y1=B,Z1=C,A2=D,B2=E,C2=F,D2=G,E2=H,F2=I,G2=J,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] 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,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):[56]: 1 with precondition: [N=0,Y=0,W1=0,V2=0,X1=A,Y1=B,Z1=C,D2=G,E2=H,F2=I,G2=J,H2=K,L2=O,M2=P,N2=Q,O2=R,P2=S,Q2=T,R2=U,S2=V,T2=W,E=X,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,D=A2,E=B2,L=I2,L=J2,L=K2,E=U2,D>=0,E>=0,L>=1,C2>=2] 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,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):[[50,51,52,53],54]: 1+it1*(1) Such that:it1=<1*D+1,it1=<1*D+ -1*A2 with precondition: [N=0,Y=0,W1=0,V2=0,W2=0,A=X1,B=Y1,C=Z1,G=D2,H=E2,I=F2,J=G2,K=H2,K2=I2,K2=J2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,A2=Z2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,D+E=A2+X,D+E=A2+B2,D+E=A2+U2,D+E=A2+Y2,0>=K2+1,E>=0,A2>=0,C2>=2,D>=A2+1] 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,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):[[50,51,52,53],55]: 0+it1*(1) Such that:it1=<1*D+1,it1=<1*D+ -1*A2 with precondition: [W1=1,A=X1,B=Y1,C=Z1,G=D2,H=E2,I=F2,J=G2,K=H2,I2=J2,N=K2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,X=U2,Y=V2,N=W2,B2=Y2,A2=Z2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,E>=0,A2+1>=0,C2>=2,B2>=E+1,D>=A2+1] 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,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):[[50,51,52,53],56]: 1+it1*(1) Such that:it1=<1*D+1,it1=<1*D+ -1*A2 with precondition: [N=0,Y=0,W1=0,V2=0,W2=0,B2=X,A=X1,B=Y1,C=Z1,G=D2,H=E2,I=F2,J=G2,K=H2,I2=J2,I2=K2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,B2=U2,B2=Y2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,D+E=A2+B2,D+E=B2+Z2,E>=0,C2>=2,I2>=1,B2>=E+1,D+E>=B2] 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,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): 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,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):[62]: 0 with precondition: [W1=1,X1=A,Y1=B,Z1=C,A2=D,B2=E,C2=F,D2=G,E2=H,F2=I,G2=J,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] 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,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):[63]: 1 with precondition: [N=0,W1=0,J3=0,L3=0,X1=A,Y1=B,Z1=C,A2=D,B2=E,D2=G,E2=H,F2=I,G2=J,H2=K,L2=O,M2=P,N2=Q,O2=R,P2=S,Q2=T,R2=U,S2=V,T2=W,W2=Z,X2=A1,Y2=B1,Z2=C1,A3=D1,B3=E1,C3=F1,D3=G1,E3=H1,F3=I1,G3=J1,P3=S1,Q3=T1,R3=U1,S3=V1,L=I2,X=U2,R1+1=V2,L=H3,R1=I3,L=K3,L=M3,L=N3,R1=O3,L>=1,X>=0,Y>=0,C2>=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,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):[64]: 1 with precondition: [N=0,W1=0,J3=0,L3=0,X1=A,Y1=B,Z1=C,A2=D,B2=E,D2=G,E2=H,F2=I,G2=J,H2=K,L2=O,M2=P,N2=Q,O2=R,P2=S,Q2=T,R2=U,S2=V,T2=W,W2=Z,X2=A1,Y2=B1,Z2=C1,A3=D1,B3=E1,C3=F1,D3=G1,E3=H1,F3=I1,G3=J1,P3=S1,Q3=T1,R3=U1,S3=V1,L=I2,X=U2,R1+1=V2,L=H3,R1=I3,L=K3,L=M3,L=N3,R1=O3,0>=L+1,X>=0,Y>=0,C2>=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,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):[[58,59,60,61],62]: 0+it1*(1) Such that:it1=<1*X+1,it1=<1*X+ -1*U2 with precondition: [W1=1,A=X1,B=Y1,C=Z1,D=A2,E=B2,G=D2,H=E2,I=F2,J=G2,K=H2,I2=J2,N=K2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,N=D3,V2=F3,U2=G3,K1=H3,L1=I3,M1=J3,N1=K3,O1=L3,P1=M3,Q1=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,U2+V2=X+Y,C2>=2,U2+1>=0,X>=U2+1,U2+V2>=X] 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,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):[[58,59,60,61],63]: 1+it1*(1) Such that:it1=<1*X+1,it1=<1*X+ -1*U2 with precondition: [N=0,W1=0,D3=0,J3=0,L3=0,A=X1,B=Y1,C=Z1,D=A2,E=B2,G=D2,H=E2,I=F2,J=G2,K=H2,K3=I2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,R1+1=V2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,U2=G3,K3=H3,R1=I3,K3=M3,K3=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,X+Y=F3+U2,Y>=0,C2>=2,U2>=0,K3>=1,X>=U2+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,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):[[58,59,60,61],64]: 1+it1*(1) Such that:it1=<1*X+1,it1=<1*X+ -1*U2 with precondition: [N=0,W1=0,D3=0,J3=0,L3=0,A=X1,B=Y1,C=Z1,D=A2,E=B2,G=D2,H=E2,I=F2,J=G2,K=H2,K3=I2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,R1+1=V2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,U2=G3,K3=H3,R1=I3,K3=M3,K3=N3,R1=O3,S1=P3,T1=Q3,U1=R3,V1=S3,X+Y=F3+U2,0>=K3+1,Y>=0,C2>=2,U2>=0,X>=U2+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,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): 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,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):[74]: 1 with precondition: [W1=1,X1=A,Y1=B,Z1=C,A2=D,B2=E,D2=G,F2=I,G2=J,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,M1=K1,I3=L1,P3=S1,Q3=T1,R3=U1,S3=V1,R1=O3,R1>=0,C2>=2] 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,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):[[66,67,68,69,70,71,72,73],74]: 1+it1*(1) Such that:it1=<1*R1+1,it1=<1*R1+ -1*O3 with precondition: [K1=0,M1=0,W1=1,A=X1,B=Y1,C=Z1,D=A2,E=B2,G=D2,I=F2,J=G2,K=H2,M=J2,N=K2,O=L2,P=M2,Q=N2,S=P2,T=Q2,U=R2,V=S2,W=T2,X=U2,Y=V2,Z=W2,A1=X2,B1=Y2,C1=Z2,D1=A3,E1=B3,F1=C3,G1=D3,H1=E3,I1=F3,J1=G3,L1=I3,O3=P3,T1=Q3,U1=R3,V1=S3,C2>=2,O3>=0,R1>=O3+1] 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,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1): 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,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1):[76]: 1 with precondition: [M1=K1,R1>=0] 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,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1):[77]: 1+it1*(1) Such that:it1=<1*R1,it1=<1*R1+1 with precondition: [K1=0,M1=0,R1>=1] Inferred cost of loop_cont_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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1): loop_cont_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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1):[79]: 0 with precondition: [] loop_cont_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,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1):[80]: 0+it1*(1) Such that:it1=<1*X+1 with precondition: [X>=0,Y>=0] 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): 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):[82]: 1 with precondition: [N=0,Y=0,E=X,0>=L+1,D>=0,E>=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):[83]: 1+it1*(1) Such that:it1=<1*E+1,it1=<1*X+1 with precondition: [N=0,Y=0,E=X,0>=L+1,D>=0,E>=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):[84]: 1 with precondition: [N=0,Y=0,E=X,D>=0,E>=0,L>=1] 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):[85]: 1+it1*(1) Such that:it1=<1*E+1,it1=<1*X+1 with precondition: [N=0,Y=0,E=X,D>=0,E>=0,L>=1] 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):[86]: 1+it1*(1) Such that:it1=<1*D,it1=<1*X,it1=<1*D+1,it1=<1*X+ -1*E with precondition: [N=0,Y=0,E>=0,X>=E+1,D+E>=X] 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):[87]: 1+it1*(1)+it2*(1) Such that:it1=<1*D,it1=<1*X,it1=<1*D+1,it1=<1*X+ -1*E,it2=<1*X+1,it2=<1*D+1*E+1 with precondition: [N=0,Y=0,E>=0,X>=E+1,D+E>=X] 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):[88]: 1+it1*(1) Such that:it1=<1*D,it1=<1*X,it1=<1*D+1,it1=<1*X+ -1*E with precondition: [N=0,Y=0,E>=0,X>=E+1,D+E>=X] 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):[89]: 1+it1*(1)+it2*(1) Such that:it1=<1*D,it1=<1*X,it1=<1*D+1,it1=<1*X+ -1*E,it2=<1*X+1,it2=<1*D+1*E+1 with precondition: [N=0,Y=0,E>=0,X>=E+1,D+E>=X] 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):[90]: 0 with precondition: [] 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):[91]: 0+it1*(1) Such that:it1=<1*D+1 with precondition: [D>=0,E>=0] Inferred cost of f21(A,B,C,D,E,F,G,H,I,J,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): f21(A,B,C,D,E,F,G,H,I,J,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):[93]: 1 with precondition: [] f21(A,B,C,D,E,F,G,H,I,J,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):[94]: 2 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[95]: 2+it1*(1) Such that:it1=<1*D+1 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[96]: 2 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[97]: 2+it1*(1) Such that:it1=<1*D+1 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[98]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[99]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[100]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[101]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[102]: 1 with precondition: [] f21(A,B,C,D,E,F,G,H,I,J,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):[103]: inf with precondition: [] Solved cost expressions of f21(A,B,C,D,E,F,G,H,I,J,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): f21(A,B,C,D,E,F,G,H,I,J,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):[93]: 1 with precondition: [] f21(A,B,C,D,E,F,G,H,I,J,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):[94]: 2 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[95]: 1*D+3 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[96]: 2 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[97]: 1*D+3 with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[98]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[99]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[100]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[101]: inf with precondition: [E=0,D>=2] f21(A,B,C,D,E,F,G,H,I,J,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):[102]: 1 with precondition: [] f21(A,B,C,D,E,F,G,H,I,J,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):[103]: inf with precondition: [] Maximum cost of f21(A,B,C,D,E,F,G,H,I,J,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): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 578 ms. Invariants computed in 2797 ms. ----Backward Invariants 1321 ms. ----Transitive Invariants 581 ms. Refinement performed in 5149 ms. Termination proved in 2278 ms. Upper bounds computed in 871 ms. ----Phase cost structures 351 ms. --------Equation cost structures 339 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 482 ms. ----Solving cost expressions 1 ms. Compressed phase information: 10 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 14991 ms.