warning: Ignored call to f9/28 in equation f8/28 warning: Ignored call to f9/28 in equation f8/28 warning: Ignored call to loop_cont_f12/28 in equation loop_cont_f1/28 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): 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):[17]: 1 with precondition: [B=2,I=2,J=2,S=2,C1=0,V1=2,D1=A,G1=D,I1=F,J1=G,K1=H,K=M,Q1=N,R1=O,S1=P,K=Q,U1=R,W1=T,X1=U,Y1=V,Z1=W,A2=X,D2=A1,K=H1,E1>=2,M1>=2,E2>=E1] 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):[18]: 0 with precondition: [J=2,S=2,C1=1,M1=2,V1=2,D1=A,F1=C,G1=D,H1=E,I1=F,J1=G,K1=H,B=I,O1=L,K=M,Q1=N,R1=O,S1=P,K=Q,U1=R,W1=T,X1=U,Y1=V,Z1=W,A2=X,B2=Y,C2=Z,D2=A1,E2=B1,B=E1,B=L1,K=N1,K=P1,K=T1,B>=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):[[16],17]: 1+it1*(1) Such that:it1=<1*B+ -1*J,it1=<1*I+ -1*J,it1=<1*R1+ -1,it1=<1*R1+ -1*J+1 with precondition: [S=2,C1=0,V1=2,B=I,K=M,A=D1,D=G1,F=I1,G=J1,H=K1,B=R1+1,P=S1,R=U1,T=W1,U=X1,V=Y1,W=Z1,X=A2,A1=D2,J>=2,E1>=2,M1>=2,B>=J+1,E2>=E1] 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):[[16],18]: 0+it1*(1) Such that:it1=<1*B+ -2,it1=<1*B+ -1*J,it1=<1*I+ -2,it1=<1*I+ -1*J,it1=<1*E1+ -2,it1=<1*L1+ -2,it1=<1*L1+ -1*J,it1=<1*M1+ -2,it1=<1*R1+ -1,it1=<1*R1+ -1*J+1 with precondition: [S=2,C1=1,V1=2,B=I,K=M,A=D1,B=E1,C=F1,D=G1,E=H1,F=I1,G=J1,H=K1,B=L1,R1+1=M1,N1=P1,P=S1,Q=T1,R=U1,T=W1,U=X1,V=Y1,W=Z1,X=A2,Y=B2,Z=C2,A1=D2,B1=E2,J>=2,R1>=J,B>=R1+1] Inferred cost of f12(A,B,C,D,E,F,G,H,I,J,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): f12(A,B,C,D,E,F,G,H,I,J,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):[21]: 1 with precondition: [C=0,E=0,C1=1,F1=0,H1=0,G1=D,I1=F,J1=G,K1=H,L1=I,M1=J,N1=K,O1=L,P1=M,Q1=N,R1=O,S1=P,T1=Q,U1=R,V1=S,B2=Y,E2=B1,A=D1,A>=0,E1>=2] f12(A,B,C,D,E,F,G,H,I,J,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):[[20],21]: inf with precondition: [E=0,C1=1,F1=0,G1=0,H1=0,A=D1,G=I1,G=J1,A=K1,I=L1,J=M1,K=N1,L=O1,M=P1,N=Q1,O=R1,P=S1,Q=T1,R=U1,S=V1,Y=B2,B1=E2,A>=0,E1>=2] f12(A,B,C,D,E,F,G,H,I,J,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):[[20],22]...: inf with precondition: [1>=C1,A>=0,C1>=0] 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): 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):[23]: 1 with precondition: [C=0,E=0,A>=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):[24]: inf with precondition: [E=0,A>=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):[25]...: inf with precondition: [A>=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):[26]...: inf with precondition: [A>=0] Inferred cost of f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1): f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[28]: 1 with precondition: [] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[29]: 1 with precondition: [L=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[30]: 3 with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[31]: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[32]: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[33]: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[34]: 1 with precondition: [] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[35]: inf with precondition: [] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[36]...: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[37]...: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[38]...: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[39]...: inf with precondition: [A>=0] Solved cost expressions of f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1): f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[28]: 1 with precondition: [] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[29]: 1 with precondition: [L=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[30]: 3 with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[31]: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[32]: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[33]: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[34]: 1 with precondition: [] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[35]: inf with precondition: [] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[36]...: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[37]...: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[38]...: inf with precondition: [A>=0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1):[39]...: inf with precondition: [A>=0] Maximum cost of f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 56 ms. Invariants computed in 247 ms. ----Backward Invariants 115 ms. ----Transitive Invariants 48 ms. Refinement performed in 259 ms. Termination proved in 135 ms. Upper bounds computed in 171 ms. ----Phase cost structures 56 ms. --------Equation cost structures 51 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 105 ms. ----Solving cost expressions 0 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1001 ms.