warning: Ignored call to f52/20 in equation f49/20 warning: Ignored call to loop_cont_f47/20 in equation f35/20 warning: Ignored call to loop_cont_f47/20 in equation f35/20 warning: Ignored call to loop_cont_f47/20 in equation f35/20 warning: Ignored call to loop_cont_f47/20 in equation loop_cont_f11/20 Warning: the following predicates are never called:[f49/20] 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): 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):[27]: 1 with precondition: [S=0,T=0,U=0,X=0,N1=0,O1=0,Y=D,Z=E,A1=F,B1=G,C1=H,D1=I,E1=J,F1=K,G1=L,H1=M,I1=N,J1=O,K1=P,L1=Q,M1=R,A=V,B=W,A>=B] 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):[28]: 0 with precondition: [S=0,T=0,U=1,N1=0,O1=0,X=C,Y=D,Z=E,A1=F,B1=G,C1=H,D1=I,E1=J,F1=K,G1=L,H1=M,I1=N,J1=O,K1=P,L1=Q,M1=R,A=V,B=W,B>=A+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):[29]: 1 with precondition: [S=0,T=0,U=0,X=0,N1=0,O1=0,E1=C,Y=D,Z=E,H1=M,I1=N,J1=O,K1=P,L1=Q,M1=R,A=V,B=W,A1=F1,A1=G1,A1>=1,B>=A+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):[30]: 0 with precondition: [S=0,T=0,U=1,N1=0,O1=0,V=A,W=B,X=C,Y=D,Z=E,A1=F,B1=G,C1=H,D1=I,E1=J,F1=K,G1=L,H1=M,I1=N,J1=O,K1=P,L1=Q,M1=R] 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):[31]: 1 with precondition: [S=0,T=0,U=0,J1=0,M1=0,N1=0,O1=0,Z=E,I1=O,A=V,B=W,C=X,C=E1,A1=F1,A1=G1,A1=H1,Y=K1,Y=L1,0>=A1,Y>=2,B>=A+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):[32]: 1 with precondition: [S=0,T=0,U=0,J1=0,M1=0,N1=0,O1=0,Z=E,I1=O,A=V,B=W,C=X,C=E1,A1=F1,A1=G1,A1=H1,Y=K1,Y=L1,0>=Y,0>=A1,B>=A+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):[[26],27]: 1+it1*(1) Such that:it1=<1*V+ -1*A,it1=<1*W+ -1*A with precondition: [S=0,T=0,U=0,X=0,Y=1,K1=1,L1=1,M1=0,N1=0,O1=0,B=V,B=W,E=Z,F1=A1,C=E1,F1=G1,F1=H1,O=I1,O=J1,0>=F1,B>=A+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):[[26],28]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*V+ -1*A with precondition: [S=0,T=0,U=1,Y=1,K1=1,L1=1,M1=0,N1=0,O1=0,B=W,C=X,E=Z,C=E1,A1=F1,A1=G1,A1=H1,O=I1,O=J1,0>=A1,V>=A+1,B>=V+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):[[26],29]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*V+ -1*A with precondition: [S=0,T=0,U=0,X=0,Y=1,K1=1,L1=1,M1=0,N1=0,O1=0,B=W,E=Z,C=E1,A1=F1,A1=G1,O=I1,O=J1,0>=H1,A1>=1,V>=A+1,B>=V+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):[[26],30]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*V+ -1*A with precondition: [S=0,T=0,U=1,Y=1,K1=1,L1=1,M1=0,N1=0,O1=0,B=W,C=X,E=Z,C=E1,A1=F1,A1=G1,A1=H1,O=I1,O=J1,0>=A1,V>=A+1,B>=V] 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):[[26],31]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*V+ -1*A with precondition: [S=0,T=0,U=0,J1=0,M1=0,N1=0,O1=0,B=W,C=X,E=Z,C=E1,A1=F1,A1=G1,A1=H1,O=I1,Y=K1,Y=L1,0>=A1,Y>=2,V>=A+1,B>=V+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):[[26],32]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*V+ -1*A with precondition: [S=0,T=0,U=0,J1=0,M1=0,N1=0,O1=0,B=W,C=X,E=Z,C=E1,A1=F1,A1=G1,A1=H1,O=I1,Y=K1,Y=L1,0>=Y,0>=A1,V>=A+1,B>=V+1] Inferred cost of f47(A,B,C,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): f47(A,B,C,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):[35]: 0 with precondition: [U=1,V=A,W=B,X=C,Y=D,Z=E,A1=F,B1=G,C1=H,D1=I,E1=J,F1=K,G1=L,H1=M,I1=N,J1=O,K1=P,L1=Q,M1=R,N1=S,O1=T] f47(A,B,C,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):[[34],35]: inf with precondition: [U=1,A=V,B=W,C=X,D=Y,E=Z,F=A1,G=B1,H=C1,I=D1,J=E1,K=F1,L=G1,M=H1,N=I1,O=J1,P=K1,Q=L1,R=M1,S=N1,T=O1] f47(A,B,C,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):[[34],36]...: inf with precondition: [1>=U,U>=0] Inferred cost of f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T): f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[37]: 1 with precondition: [D>=3] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[38]: inf with precondition: [D>=3] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[39]: 1 with precondition: [1>=D] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[40]: inf with precondition: [1>=D] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[41]: 1 with precondition: [D=2] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[42]: inf with precondition: [D=2] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[43]...: inf with precondition: [D>=3] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[44]...: inf with precondition: [D>=3] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[45]...: inf with precondition: [1>=D] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[46]...: inf with precondition: [1>=D] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[47]...: inf with precondition: [D=2] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[48]...: inf with precondition: [D=2] 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): loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[50]: 1 with precondition: [D>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[51]: inf with precondition: [D>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[52]: 1 with precondition: [1>=D] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[53]: inf with precondition: [1>=D] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[54]: 1 with precondition: [D=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[55]: inf with precondition: [D=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[56]: 0 with precondition: [] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[57]: inf with precondition: [] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[58]...: inf with precondition: [D>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[59]...: inf with precondition: [D>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[60]...: inf with precondition: [1>=D] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[61]...: inf with precondition: [1>=D] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[62]...: inf with precondition: [D=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[63]...: inf with precondition: [D=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[64]...: inf with precondition: [] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[65]...: inf with precondition: [] Inferred cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[67]: 3 with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[68]: inf with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[69]: 3 with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[70]: inf with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[71]: 3 with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[72]: inf with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[73]: 2 with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[74]: inf with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[75]: 3 with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[76]: inf with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[77]: 3 with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[78]: inf with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[79]: 3 with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[80]: inf with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[81]: 2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[82]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[83]: 3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[84]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[85]: 3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[86]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[87]: 2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[88]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[89]: 3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[90]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[91]: 2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[92]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[93]: 3+it1*(1) Such that:it1=<1*B+ -1*A with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[94]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[95]: 2+it1*(1) Such that:it1=<1*B+ -1*A with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[96]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[97]: 3+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[98]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[99]: 2+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[100]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[101]: 3+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[102]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[103]: 3+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[104]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[105]: 2+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[106]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[107]: 3+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[108]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[109]: 2+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[110]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[111]: 1 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[112]: 1 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[113]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<-1*A+1*B+ -1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[114]: 1+it1*(1) Such that:it1=<-1*A+1*B,it1=<1*B+ -1*A with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[115]...: inf with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[116]...: inf with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[117]...: inf with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[118]...: inf with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[119]...: inf with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[120]...: inf with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[121]...: inf with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[122]...: inf with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[123]...: inf with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[124]...: inf with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[125]...: inf with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[126]...: inf with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[127]...: inf with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[128]...: inf with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[129]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[130]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[131]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[132]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[133]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[134]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[135]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[136]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[137]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[138]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[139]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[140]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[141]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[142]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[143]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[144]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[145]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[146]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[147]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[148]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[149]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[150]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[151]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[152]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[153]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[154]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[155]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[156]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[157]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[158]...: inf with precondition: [B>=A+2] Solved cost expressions of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[67]: 3 with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[68]: inf with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[69]: 3 with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[70]: inf with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[71]: 3 with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[72]: inf with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[73]: 2 with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[74]: inf with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[75]: 3 with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[76]: inf with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[77]: 3 with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[78]: inf with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[79]: 3 with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[80]: inf with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[81]: 2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[82]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[83]: 3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[84]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[85]: 3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[86]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[87]: 2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[88]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[89]: 3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[90]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[91]: 2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[92]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[93]: -1*A+1*B+3 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[94]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[95]: -1*A+1*B+2 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[96]: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[97]: -1*A+1*B+2 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[98]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[99]: -1*A+1*B+1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[100]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[101]: -1*A+1*B+2 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[102]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[103]: -1*A+1*B+2 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[104]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[105]: -1*A+1*B+1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[106]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[107]: -1*A+1*B+2 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[108]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[109]: -1*A+1*B+1 with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[110]: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[111]: 1 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[112]: 1 with precondition: [] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[113]: -1*A+1*B with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[114]: -1*A+1*B+1 with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[115]...: inf with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[116]...: inf with precondition: [D>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[117]...: inf with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[118]...: inf with precondition: [1>=D,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[119]...: inf with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[120]...: inf with precondition: [D=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[121]...: inf with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[122]...: inf with precondition: [A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[123]...: inf with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[124]...: inf with precondition: [D>=3,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[125]...: inf with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[126]...: inf with precondition: [1>=D,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[127]...: inf with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[128]...: inf with precondition: [D=2,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[129]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[130]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[131]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[132]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[133]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[134]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[135]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[136]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[137]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[138]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[139]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[140]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[141]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[142]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[143]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[144]...: inf with precondition: [B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[145]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[146]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[147]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[148]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[149]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[150]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[151]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[152]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[153]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[154]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[155]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[156]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[157]...: inf with precondition: [B>=A+2] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T):[158]...: inf with precondition: [B>=A+2] Maximum cost of f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 64 ms. Invariants computed in 246 ms. ----Backward Invariants 155 ms. ----Transitive Invariants 25 ms. Refinement performed in 493 ms. Termination proved in 62 ms. Upper bounds computed in 399 ms. ----Phase cost structures 245 ms. --------Equation cost structures 235 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 123 ms. ----Solving cost expressions 5 ms. Compressed phase information: 12 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1396 ms.