warning: Ignored call to loop_cont_f1/13 in equation f0/13 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): 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):[22]: 2 with precondition: [A=0,D=3,F=0,I=3,K=2,N=0,R=2,W=2,Y=1,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,S=X,7>=E,1>=O,7>=S,E>=1,O>=0,S>=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):[23]: 1 with precondition: [A=0,D=3,F=0,I=3,K=2,N=1,S=2,X=2,Y=4,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,R=W,7>=E,1>=O,7>=R,E>=1,O>=0,R>=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):[24]: 2 with precondition: [A=0,D=3,F=0,I=3,K=2,N=0,R=2,W=2,Y=1,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,S=X,7>=E,1>=O,7>=S,E>=1,O>=0,S>=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):[25]: 2 with precondition: [A=0,D=3,F=0,I=3,K=2,N=0,R=2,W=2,Y=1,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,S=X,7>=E,1>=O,7>=S,E>=1,O>=0,S>=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):[26]: 1 with precondition: [A=0,D=3,F=0,I=3,K=2,N=1,S=7,X=7,Y=4,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,R=W,7>=E,1>=O,7>=R,E>=1,O>=0,R>=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):[27]: 2 with precondition: [A=0,D=3,F=0,I=3,K=2,N=0,R=2,W=2,Y=1,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,S=X,7>=E,1>=O,7>=S,E>=1,O>=0,S>=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):[28]: 1 with precondition: [A=0,D=3,F=0,I=3,K=2,N=0,R=2,W=2,Y=1,G=B,H=C,E=J,Z=L,A1=M,U=P,V=Q,O=T,S=X,7>=E,1>=O,7>=S,E>=1,O>=0,S>=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):[29]: 0 with precondition: [A=0,D=3,F=0,I=3,K=2,N=1,O=0,R=3,T=0,W=3,Y=2,G=B,H=C,E=J,Z=L,A1=M,G=P,H=Q,E=S,G=U,H=V,E=X,7>=E,E>=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):[[20,21],22]: inf with precondition: [A=0,F=0,K=2,N=0,R=2,W=2,Y=1,B=G,C=H,D=I,E=J,T=O,X=S,P=U,Q=V,L=Z,M=A1,7>=D,7>=E,1>=T,7>=X,D>=1,E>=1,L>=1,M>=1,T>=0,X>=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):[[20,21],23]: inf with precondition: [A=0,F=0,K=2,N=1,S=2,X=2,Y=4,B=G,C=H,D=I,E=J,O=T,P=U,Q=V,R=W,L=Z,M=A1,7>=D,7>=E,1>=O,7>=R,D>=1,E>=1,L>=1,M>=1,O>=0,R>=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):[[20,21],24]: inf with precondition: [A=0,F=0,K=2,N=0,R=2,W=2,Y=1,B=G,C=H,D=I,E=J,O=T,P=U,Q=V,S=X,L=Z,M=A1,7>=D,7>=E,1>=O,7>=S,D>=1,E>=1,L>=1,M>=1,O>=0,S>=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):[[20,21],25]: inf with precondition: [A=0,F=0,K=2,N=0,R=2,W=2,Y=1,B=G,C=H,D=I,E=J,O=T,P=U,Q=V,S=X,L=Z,M=A1,7>=D,7>=E,1>=O,7>=S,D>=1,E>=1,L>=1,M>=1,O>=0,S>=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):[[20,21],26]: inf with precondition: [A=0,F=0,K=2,N=1,S=7,X=7,Y=4,B=G,C=H,D=I,E=J,O=T,P=U,Q=V,R=W,L=Z,M=A1,7>=D,7>=E,1>=O,7>=R,D>=1,E>=1,L>=1,M>=1,O>=0,R>=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):[[20,21],27]: inf with precondition: [A=0,F=0,K=2,N=0,R=2,W=2,Y=1,B=G,C=H,D=I,E=J,O=T,P=U,Q=V,S=X,L=Z,M=A1,7>=D,7>=E,1>=O,7>=S,D>=1,E>=1,L>=1,M>=1,O>=0,S>=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):[[20,21],28]: inf with precondition: [A=0,F=0,K=2,N=0,R=2,W=2,Y=1,B=G,C=H,D=I,E=J,O=T,P=U,Q=V,S=X,L=Z,M=A1,7>=D,7>=E,1>=O,7>=S,D>=1,E>=1,L>=1,M>=1,O>=0,S>=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):[[20,21],29]: inf with precondition: [A=0,F=0,K=2,N=1,O=0,T=0,Y=2,B=G,C=H,D=I,E=J,P=U,Q=V,R=W,S=X,L=Z,M=A1,7>=D,7>=E,7>=R,7>=S,D>=1,E>=1,L>=1,M>=1,R>=1,S>=1,M>=P+1,L>=Q+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):[[20,21],30]...: inf with precondition: [A=0,F=0,K=2,B=G,C=H,D=I,E=J,7>=D,7>=E,1>=N,D>=1,E>=1,L>=1,M>=1,N>=0] 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): 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):[42]: 2 with precondition: [N=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):[43]: 2 with precondition: [N=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):[44]: 1 with precondition: [N=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):[45]: inf with precondition: [N=1,L>=1,M>=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):[46]: inf with precondition: [N=1,L>=1,M>=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):[47]: inf with precondition: [N=1,L>=1,M>=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):[48]: 0 with precondition: [N=1,O=A,P=B,Q=C,R=D,S=E,T=F,U=G,V=H,W=I,X=J,Y=K,Z=L,A1=M] 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):[49]...: inf with precondition: [1>=N,L>=1,M>=1,N>=0] 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):[50]...: inf with precondition: [N=1,L>=1,M>=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):[[31,32,33,34,35,36,37,38,39,40,41],42]: inf with precondition: [N=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):[[31,32,33,34,35,36,37,38,39,40,41],43]: inf with precondition: [N=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):[[31,32,33,34,35,36,37,38,39,40,41],44]: inf with precondition: [N=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):[[31,32,33,34,35,36,37,38,39,40,41],45]: inf with precondition: [N=1,L>=1,M>=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):[[31,32,33,34,35,36,37,38,39,40,41],46]: inf with precondition: [N=1,L>=1,M>=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):[[31,32,33,34,35,36,37,38,39,40,41],47]: inf with precondition: [N=1,L>=1,M>=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):[[31,32,33,34,35,36,37,38,39,40,41],48]: inf with precondition: [N=1,R=2,W=2,Y=1,T=O,X=S,P=U,Q=V,L=Z,M=A1,1>=T,7>=X,T>=0,X>=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):[[31,32,33,34,35,36,37,38,39,40,41],49]...: inf with precondition: [1>=N,L>=1,M>=1,N>=0] 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):[[31,32,33,34,35,36,37,38,39,40,41],50]...: inf with precondition: [N=1,L>=1,M>=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):[[31,32,33,34,35,36,37,38,39,40,41],51]...: inf with precondition: [1>=N,N>=0] Inferred cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M): f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[52]: 3 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[53]: 3 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[54]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[55]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[56]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[57]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[58]: 1 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[59]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[60]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[61]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[62]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[63]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[64]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[65]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[66]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[67]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[68]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[69]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[70]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[71]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[72]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[73]...: inf with precondition: [] Solved cost expressions of f0(A,B,C,D,E,F,G,H,I,J,K,L,M): f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[52]: 3 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[53]: 3 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[54]: 2 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[55]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[56]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[57]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[58]: 1 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[59]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[60]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[61]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[62]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[63]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[64]: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[65]: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[66]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[67]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[68]...: inf with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[69]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[70]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[71]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[72]...: inf with precondition: [L>=1,M>=1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M):[73]...: inf with precondition: [] Maximum cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 68 ms. Invariants computed in 672 ms. ----Backward Invariants 508 ms. ----Transitive Invariants 40 ms. Refinement performed in 347 ms. Termination proved in 89 ms. Upper bounds computed in 275 ms. ----Phase cost structures 66 ms. --------Equation cost structures 65 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 195 ms. ----Solving cost expressions 1 ms. Compressed phase information: 25 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1531 ms.