warning: Ignored call to f56/22 in equation f53/22 warning: Ignored call to loop_cont_f51/22 in equation f37/22 warning: Ignored call to loop_cont_f51/22 in equation f37/22 warning: Ignored call to loop_cont_f51/22 in equation f37/22 warning: Ignored call to loop_cont_f51/22 in equation loop_cont_f11/22 Warning: the following predicates are never called:[f53/22] 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,P1,Q1,R1,S1): 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,P1,Q1,R1,S1):[27]: 1 with precondition: [C=0,V=0,W=0,Z=0,A1=0,S1=0,B1=E,C1=F,D1=G,E1=H,F1=I,G1=J,H1=K,I1=L,J1=M,K1=N,L1=O,M1=P,N1=Q,O1=R,P1=S,Q1=T,R1=U,A=X,B=Y,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,P1,Q1,R1,S1):[28]: 0 with precondition: [C=0,V=0,W=1,Z=0,S1=0,A1=D,B1=E,C1=F,D1=G,E1=H,F1=I,G1=J,H1=K,I1=L,J1=M,K1=N,L1=O,M1=P,N1=Q,O1=R,P1=S,Q1=T,R1=U,A=X,B=Y,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,P1,Q1,R1,S1):[29]: 1 with precondition: [C=0,V=0,W=0,Z=0,A1=0,S1=0,H1=D,B1=E,C1=F,L1=O,M1=P,N1=Q,O1=R,P1=S,Q1=T,R1=U,A=X,B=Y,D1=I1,D1=J1,D1=K1,D1>=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,P1,Q1,R1,S1):[30]: 0 with precondition: [C=0,V=0,W=1,Z=0,S1=0,X=A,Y=B,A1=D,B1=E,C1=F,D1=G,E1=H,F1=I,G1=J,H1=K,I1=L,J1=M,K1=N,L1=O,M1=P,N1=Q,O1=R,P1=S,Q1=T,R1=U] 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,P1,Q1,R1,S1):[31]: 1 with precondition: [C=0,V=0,W=0,Z=0,N1=0,R1=0,S1=0,C1=F,M1=Q,A=X,B=Y,D=A1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,B1=O1,B1=P1,B1=Q1,0>=D1,B1>=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,P1,Q1,R1,S1):[32]: 1 with precondition: [C=0,V=0,W=0,Z=0,N1=0,R1=0,S1=0,C1=F,M1=Q,A=X,B=Y,D=A1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,B1=O1,B1=P1,B1=Q1,0>=B1,0>=D1,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,P1,Q1,R1,S1):[[26],27]: 1+it1*(1) Such that:it1=<1*X+ -1*A,it1=<1*Y+ -1*A with precondition: [C=0,V=0,W=0,Z=0,A1=0,B1=1,O1=1,P1=1,Q1=1,R1=0,S1=0,B=X,B=Y,F=C1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,Q=M1,Q=N1,0>=D1,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,P1,Q1,R1,S1):[[26],28]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*X+ -1*A with precondition: [C=0,V=0,W=1,Z=0,B1=1,O1=1,P1=1,Q1=1,R1=0,S1=0,B=Y,D=A1,F=C1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,Q=M1,Q=N1,0>=D1,X>=A+1,B>=X+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,P1,Q1,R1,S1):[[26],29]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*X+ -1*A with precondition: [C=0,V=0,W=0,Z=0,A1=0,B1=1,O1=1,P1=1,Q1=1,R1=0,S1=0,B=Y,F=C1,D=H1,D1=I1,D1=J1,D1=K1,Q=M1,Q=N1,0>=L1,D1>=1,X>=A+1,B>=X+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,P1,Q1,R1,S1):[[26],30]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*X+ -1*A with precondition: [C=0,V=0,W=1,Z=0,B1=1,O1=1,P1=1,Q1=1,R1=0,S1=0,B=Y,D=A1,F=C1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,Q=M1,Q=N1,0>=D1,X>=A+1,B>=X] 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,P1,Q1,R1,S1):[[26],31]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*X+ -1*A with precondition: [C=0,V=0,W=0,Z=0,N1=0,R1=0,S1=0,B=Y,D=A1,F=C1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,Q=M1,B1=O1,B1=P1,B1=Q1,0>=D1,B1>=2,X>=A+1,B>=X+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,P1,Q1,R1,S1):[[26],32]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*X+ -1*A with precondition: [C=0,V=0,W=0,Z=0,N1=0,R1=0,S1=0,B=Y,D=A1,F=C1,D=H1,D1=I1,D1=J1,D1=K1,D1=L1,Q=M1,B1=O1,B1=P1,B1=Q1,0>=B1,0>=D1,X>=A+1,B>=X+1] Inferred cost of f51(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): f51(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):[35]: 0 with precondition: [W=1,X=A,Y=B,Z=C,A1=D,B1=E,C1=F,D1=G,E1=H,F1=I,G1=J,H1=K,I1=L,J1=M,K1=N,L1=O,M1=P,N1=Q,O1=R,P1=S,Q1=T,R1=U,S1=V] f51(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):[[34],35]: inf with precondition: [W=1,A=X,B=Y,C=Z,D=A1,E=B1,F=C1,G=D1,H=E1,I=F1,J=G1,K=H1,L=I1,M=J1,N=K1,O=L1,P=M1,Q=N1,R=O1,S=P1,T=Q1,U=R1,V=S1] f51(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):[[34],36]...: inf with precondition: [1>=W,W>=0] Inferred cost of f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V): f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[37]: 1 with precondition: [E>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[38]: inf with precondition: [E>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[39]: 1 with precondition: [1>=E] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[40]: inf with precondition: [1>=E] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[41]: 1 with precondition: [E=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[42]: inf with precondition: [E=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[43]...: inf with precondition: [E>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[44]...: inf with precondition: [E>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[45]...: inf with precondition: [1>=E] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[46]...: inf with precondition: [1>=E] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[47]...: inf with precondition: [E=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[48]...: inf with precondition: [E=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,U,V): loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[50]: 1 with precondition: [E>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[51]: inf with precondition: [E>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[52]: 1 with precondition: [1>=E] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[53]: inf with precondition: [1>=E] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[54]: 1 with precondition: [E=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[55]: inf with precondition: [E=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[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,U,V):[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,U,V):[58]...: inf with precondition: [E>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[59]...: inf with precondition: [E>=3] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[60]...: inf with precondition: [1>=E] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[61]...: inf with precondition: [1>=E] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[62]...: inf with precondition: [E=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[63]...: inf with precondition: [E=2] loop_cont_f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[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,U,V):[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,U,V): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[67]: 3 with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[68]: inf with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[69]: 3 with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[70]: inf with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[71]: 3 with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[72]: inf with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[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,U,V):[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,U,V):[75]: 3 with precondition: [E>=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,U,V):[76]: inf with precondition: [E>=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,U,V):[77]: 3 with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[78]: inf with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[79]: 3 with precondition: [E=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,U,V):[80]: inf with precondition: [E=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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[115]...: inf with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[116]...: inf with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[117]...: inf with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[118]...: inf with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[119]...: inf with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[120]...: inf with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[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,U,V):[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,U,V):[123]...: inf with precondition: [E>=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,U,V):[124]...: inf with precondition: [E>=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,U,V):[125]...: inf with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[126]...: inf with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[127]...: inf with precondition: [E=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,U,V):[128]...: inf with precondition: [E=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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[67]: 3 with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[68]: inf with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[69]: 3 with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[70]: inf with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[71]: 3 with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[72]: inf with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[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,U,V):[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,U,V):[75]: 3 with precondition: [E>=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,U,V):[76]: inf with precondition: [E>=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,U,V):[77]: 3 with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[78]: inf with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[79]: 3 with precondition: [E=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,U,V):[80]: inf with precondition: [E=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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[115]...: inf with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[116]...: inf with precondition: [E>=3,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[117]...: inf with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[118]...: inf with precondition: [1>=E,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[119]...: inf with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[120]...: inf with precondition: [E=2,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[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,U,V):[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,U,V):[123]...: inf with precondition: [E>=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,U,V):[124]...: inf with precondition: [E>=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,U,V):[125]...: inf with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[126]...: inf with precondition: [1>=E,B>=A+1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V):[127]...: inf with precondition: [E=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,U,V):[128]...: inf with precondition: [E=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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V):[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,U,V): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 80 ms. Invariants computed in 301 ms. ----Backward Invariants 190 ms. ----Transitive Invariants 31 ms. Refinement performed in 601 ms. Termination proved in 77 ms. Upper bounds computed in 483 ms. ----Phase cost structures 300 ms. --------Equation cost structures 286 ms. --------Inductive compression(1) 1 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 146 ms. ----Solving cost expressions 5 ms. Compressed phase information: 12 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1707 ms.