warning: Ignored call to f4/32 in equation f3/32 warning: Ignored call to f4/32 in equation f3/32 warning: Ignored call to f4/32 in equation f9/32 warning: Ignored call to f4/32 in equation f9/32 warning: Ignored call to loop_cont_f10/32 in equation f9/32 warning: Ignored call to loop_cont_f10/32 in equation f9/32 warning: Ignored call to loop_cont_f10/32 in equation f9/32 warning: Ignored call to loop_cont_f10/32 in equation f9/32 warning: Ignored call to loop_cont_f10/32 in equation loop_cont_f1/32 Warning: the following predicates are never called:[f9/32] Inferred cost of f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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): f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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):[20]: 0 with precondition: [B=2,G1=1,I1=2,K1=D,C=E,M1=F,N1=G,O1=H,P1=I,Q1=J,R1=K,T1=M,L=N,A=O,W1=P,X1=Q,Y1=R,Z1=S,A2=T,B2=U,C2=V,D2=W,E2=X,F2=Y,L=Z,H2=A1,C=B1,J2=C1,K2=D1,L2=E1,M2=F1,A=H1,C=J1,C=L1,L=S1,L=U1,A=V1,L=G2,C=I2,A>=2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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):[21]: 1 with precondition: [A=2,B=2,O=2,G1=0,C=E,M1=F,N1=G,O1=H,L=N,B2=U,C2=V,D2=W,E2=X,F2=Y,L=Z,C=B1,J2=C1,I=P1,C=Q1,T=R1,L=S1,L=T1,L=U1,C=W1,C=X1,C=Y1,T=A2,T+1=K2,I=L2,I1>=2,V1>=2,C>=L+1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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):[22]: 1 with precondition: [A=2,B=2,O=2,G1=0,C=E,M1=F,N1=G,O1=H,L=N,B2=U,C2=V,D2=W,E2=X,F2=Y,L=Z,C=B1,J2=C1,I=P1,C=Q1,T=R1,L=S1,L=T1,L=U1,C=W1,C=X1,C=Y1,T=A2,T+1=K2,I=L2,I1>=2,V1>=2,L>=C+1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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):[[19],20]: 0+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*O+ -2,it1=<1*O+ -1*B,it1=<1*H1+ -2,it1=<1*I1+ -2,it1=<1*N1+ -1,it1=<1*V1+ -2,it1=<1*N1+ -1*B+1 with precondition: [G1=1,C=E,L=N,A=O,L=Z,A=H1,N1+1=I1,J1=L1,I=O1,I=P1,J=Q1,K=R1,L=S1,M=T1,L=U1,A=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,L=G2,A1=H2,B1=I2,C1=J2,D1=K2,E1=L2,F1=M2,B>=2,N1>=B,A>=N1+1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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):[[19],21]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*O+ -2,it1=<1*O+ -1*B,it1=<1*N1+ -1 with precondition: [G1=0,C=E,L=N,A=O,L=Z,A=N1+1,I=O1,I=P1,X1=Q1,T=R1,L=S1,L=T1,L=U1,X1=W1,X1=Y1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,C1=J2,T+1=K2,I=L2,B>=2,I1>=2,V1>=2,A>=B+1,X1>=L+1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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):[[19],22]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*O+ -2,it1=<1*O+ -1*B,it1=<1*N1+ -1 with precondition: [G1=0,C=E,L=N,A=O,L=Z,A=N1+1,I=O1,I=P1,X1=Q1,T=R1,L=S1,L=T1,L=U1,X1=W1,X1=Y1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,C1=J2,T+1=K2,I=L2,B>=2,I1>=2,V1>=2,A>=B+1,L>=X1+1] 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): 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):[28]: 1 with precondition: [G1=1,H1=A,I1=B,J1=C,K1=D,L1=E,M1=F,N1=G,O1=H,P1=I,M=J,R1=K,S1=L,U1=N,W1=P,B2=U,C2=V,D2=W,E2=X,F2=Y,G2=Z,H2=A1,I2=B1,J2=C1,K2=D1,L2=E1,M2=F1,T=A2,T>=0,V1>=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):[[24,25,26,27],28]: 1+it1*(1) Such that:it1=<1*T+1,it1=<1*T+ -1*A2 with precondition: [G1=1,J=M,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,G=N1,H=O1,I=P1,K=R1,J=S1,J=U1,I=C2,A2=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,E1=L2,F1=M2,V1>=2,A2>=0,T>=A2+1] Inferred cost of loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1): loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[30]: 1 with precondition: [M=J,T>=0] loop_cont_f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[31]: 1+it1*(1) Such that:it1=<1*T,it1=<1*T+1 with precondition: [M=J,T>=1] Inferred cost of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1): f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[33]: 1 with precondition: [] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[34]: 1 with precondition: [] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[35]: inf with precondition: [] Solved cost expressions of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1): f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[33]: 1 with precondition: [] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[34]: 1 with precondition: [] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[35]: inf with precondition: [] Maximum cost of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 106 ms. Invariants computed in 437 ms. ----Backward Invariants 184 ms. ----Transitive Invariants 94 ms. Refinement performed in 627 ms. Termination proved in 336 ms. Upper bounds computed in 209 ms. ----Phase cost structures 51 ms. --------Equation cost structures 48 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 146 ms. ----Solving cost expressions 0 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 2063 ms.