warning: Ignored call to loop_cont_f8/27 in equation loop_cont_f2/27 Inferred cost of f2(A,B,C,D,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): f2(A,B,C,D,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):[21]: 1 with precondition: [G=2,H=1,I=1,J=2,N=2,X=2,Z=0,B1=0,I1=2,J1=1,K1=1,L1=2,P1=2,Z1=2,B2=0,E=F,M1=K,N1=L,O1=M,Q1=O,R1=P,R=S,R=T,R=U,X1=V,Y1=W,A2=Y,A=C1,D1=E1,D1=F1,E=G1,E=H1,R=T1,R=U1,R=V1,A>=D1+1] f2(A,B,C,D,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):[22]: 0 with precondition: [G=2,H=1,I=1,J=2,N=2,X=2,Z=0,B1=1,I1=2,J1=1,K1=1,L1=2,P1=2,Z1=2,B2=0,C1=A,D1=B,E1=C,F1=D,G1=E,H1=F,M1=K,N1=L,O1=M,Q1=O,R1=P,S1=Q,R=S,R=T,R=U,X1=V,Y1=W,A2=Y,C2=A1,R=T1,R=U1,R=V1,R=W1] f2(A,B,C,D,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):[23]: 1 with precondition: [G=2,H=1,I=1,J=2,N=2,X=2,Z=0,B1=0,I1=2,J1=1,K1=1,L1=2,P1=2,Z1=2,B2=0,E=F,M1=K,N1=L,O1=M,Q1=O,R1=P,R=S,R=T,R=U,X1=V,Y1=W,A2=Y,A=C1,D1=E1,D1=F1,E=G1,E=H1,R=T1,R=U1,R=V1,D1>=A+1] f2(A,B,C,D,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):[[19,20],21]: 1+it1*(1) Such that:it1=<1,it1=<2 with precondition: [G=2,H=1,I=1,J=2,N=2,X=2,Z=0,B1=0,I1=1,J1=2,K1=2,L1=1,O1=1,P1=2,Z1=2,B2=0,R=S,R=T,R=U,A=C1,F1=D1,F1=E1,E=G1,E=H1,O=Q1,P=R1,R=T1,R=U1,R=V1,V=X1,W=Y1,Y=A2,A>=F1+1] f2(A,B,C,D,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):[[19,20],22]: 0+it1*(1) Such that:it1=<2,it1=<1*G,it1=<1*J,it1=<-1*H+3,it1=<-1*I+3,it1=<-1*I1+2,it1=<-1*L1+2,it1=<-1*O1+2,it1=<1*G+ -1*O1,it1=<1*J+ -1*O1,it1=<1*J1+ -1,it1=<1*K1+ -1,it1=<-1*H+ -1*O1+3,it1=<-1*I+ -1*O1+3 with precondition: [N=2,X=2,Z=0,B1=1,P1=2,Z1=2,B2=0,G=J,R=S,R=T,R=U,A=C1,B=D1,C=E1,D=F1,E=G1,I1=L1,I1=O1,O=Q1,P=R1,Q=S1,R=T1,R=U1,R=V1,R=W1,V=X1,W=Y1,Y=A2,A1=C2,G+H=3,G+I=3,I1+J1=3,I1+K1=3,2>=G,I1>=0,G>=I1+1] f2(A,B,C,D,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):[[19,20],23]: 1+it1*(1) Such that:it1=<1,it1=<2 with precondition: [G=2,H=1,I=1,J=2,N=2,X=2,Z=0,B1=0,I1=1,J1=2,K1=2,L1=1,O1=1,P1=2,Z1=2,B2=0,R=S,R=T,R=U,A=C1,F1=D1,F1=E1,E=G1,E=H1,O=Q1,P=R1,R=T1,R=U1,R=V1,V=X1,W=Y1,Y=A2,F1>=A+1] 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,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): 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,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):[27]: 0 with precondition: [B1=1,C1=A,D1=B,E1=C,F1=D,G1=E,H1=F,I1=G,J1=H,K1=I,L1=J,M1=K,N1=L,O1=M,P1=N,Q1=O,R1=P,S1=Q,T1=R,U1=S,V1=T,W1=U,X1=V,Y1=W,Z1=X,A2=Y,B2=Z,C2=A1] 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,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):[[25],27]: inf with precondition: [B1=1,D1=B,A=C1,D1=E1,D1=F1,E=G1,F=H1,G=I1,H=J1,I=K1,J=L1,K=M1,L=N1,M=O1,N=P1,O=Q1,P=R1,Q=S1,R=T1,S=U1,T=V1,U=W1,V=X1,W=Y1,X=Z1,Y=A2,Z=B2,A1=C2,A>=D1+1] 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,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):[[25],28]...: inf with precondition: [1>=B1,B1>=0,A>=B+1] 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,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):[[26],27]: inf with precondition: [B1=1,D1=B,A=C1,D1=E1,D1=F1,E=G1,F=H1,G=I1,H=J1,I=K1,J=L1,K=M1,L=N1,M=O1,N=P1,O=Q1,P=R1,Q=S1,R=T1,S=U1,T=V1,U=W1,V=X1,W=Y1,X=Z1,Y=A2,Z=B2,A1=C2,D1>=A+1] 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,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):[[26],28]...: inf with precondition: [1>=B1,B1>=0,B>=A+1] Inferred cost of loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[29]: 0 with precondition: [] loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[30]: inf with precondition: [A>=B+1] loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[31]: inf with precondition: [B>=A+1] loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[32]...: inf with precondition: [A>=B+1] loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[33]...: inf with precondition: [B>=A+1] loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[34]...: inf with precondition: [A>=B+1] loop_cont_f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[35]...: inf with precondition: [B>=A+1] Inferred cost of f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[37]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[38]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[39]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[40]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[41]: 2+it1*(1) Such that:it1=<1,it1=<2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[42]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[43]: 2+it1*(1) Such that:it1=<1,it1=<2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[44]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[45]: 1 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[46]: 1+it1*(1) Such that:it1=<2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[47]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[48]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[49]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[50]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[51]: 2+it1*(1) Such that:it1=<1,it1=<2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[52]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[53]: 2+it1*(1) Such that:it1=<1,it1=<2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[54]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[55]: 1 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[56]: 1+it1*(1) Such that:it1=<2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[57]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[58]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[59]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[60]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[61]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[62]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[63]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[64]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[65]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[66]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[67]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[68]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[69]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[70]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[71]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[72]...: inf with precondition: [] Solved cost expressions of f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[37]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[38]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[39]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[40]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[41]: 3 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[42]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[43]: 3 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[44]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[45]: 1 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[46]: 3 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[47]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[48]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[49]: 2 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[50]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[51]: 3 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[52]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[53]: 3 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[54]: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[55]: 1 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[56]: 3 with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[57]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[58]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[59]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[60]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[61]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[62]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[63]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[64]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[65]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[66]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[67]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[68]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[69]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[70]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[71]...: inf with precondition: [] f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[72]...: inf with precondition: [] Maximum cost of f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 83 ms. Invariants computed in 425 ms. ----Backward Invariants 212 ms. ----Transitive Invariants 74 ms. Refinement performed in 557 ms. Termination proved in 269 ms. Upper bounds computed in 324 ms. ----Phase cost structures 126 ms. --------Equation cost structures 118 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 184 ms. ----Solving cost expressions 1 ms. Compressed phase information: 5 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1856 ms.