warning: Ignored call to loop_cont_f91/32 in equation f85/32 warning: Ignored call to loop_cont_f91/32 in equation f85/32 warning: Ignored call to loop_cont_f91/32 in equation f85/32 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,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,F2,G2,H2,I2,J2,K2,L2,M2): 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,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,F2,G2,H2,I2,J2,K2,L2,M2):[[56],57]: 1+it1*(1) Such that:it1=<8,it1=<-1*L+8 with precondition: [J=0,G1=0,Q1=0,S1=8,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,G=N1,H+1=O1,I=P1,M=T1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,E1=L2,R1=M2,255>=H,7>=L,L>=0] Inferred cost of f17(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,F2,G2,H2,I2,J2,K2,L2,M2): f17(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,F2,G2,H2,I2,J2,K2,L2,M2):[[59],60]: 1+it1*(2+it2*(1)) Such that:it1=<256,it1=<-1*H+256 it2=<8 with precondition: [A=1,B=40,C=0,D=40,E=0,F=1,G=0,G1=0,H1=1,I1=40,J1=0,K1=40,L1=0,M1=1,N1=0,O1=256,Q1=0,S1=8,M=T1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,E1=L2,R1=M2,255>=H] Inferred cost of f42(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,F2,G2,H2,I2,J2,K2,L2,M2): f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[64]: 1 with precondition: [H=1,G1=0,O1=1,H1=A,I1=B,J1=C,L1=E,P1=I,Q1=J,R1=K,S1=L,T1=M,U1=N,W1=P,X1=Q,Y1=R,Z1=S,A2=T,B2=U,C2=V,D2=W,E2=X,F2=Y,G2=Z,H2=A1,I2=B1,J2=C1,K2=D1,M2=F1,D=K1,F=M1,G=N1,G=V1,G=L2,0>=D,F>=0] f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[65]: 0 with precondition: [H=1,G1=1,O1=1,H1=A,I1=B,J1=C,K1=D,L1=E,M1=F,N1=G,P1=I,Q1=J,R1=K,S1=L,T1=M,U1=N,V1=O,W1=P,X1=Q,Y1=R,Z1=S,A2=T,B2=U,C2=V,D2=W,E2=X,F2=Y,G2=Z,H2=A1,I2=B1,J2=C1,K2=D1,L2=E1,M2=F1] f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[66]: 1 with precondition: [H=1,G1=0,O1=1,H1=A,I1=B,J1=C,L1=E,N1=G,P1=I,Q1=J,R1=K,S1=L,T1=M,U1=N,W1=P,X1=Q,Y1=R,Z1=S,A2=T,B2=U,C2=V,D2=W,E2=X,F2=Y,G2=Z,H2=A1,I2=B1,J2=C1,K2=D1,M2=F1,D=K1,F=M1,L2=V1,0>=D,0>=F+1] f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[[62],65]: 0+it1*(1) Such that:it1=<1*D,it1=<1*K1,it1=<1*O1+ -1,it1=<1*O1+ -1*H,it1=<1*D+ -1*H+1,it1=<1*K1+ -1*H+1 with precondition: [G1=1,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,I=P1,J=Q1,K=R1,L=S1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,E1=L2,F1=M2,0>=F+1,H>=1,O1>=H+1,D+1>=O1] f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[[62],66]: 1+it1*(1) Such that:it1=<1*K1,it1=<1*O1+ -1,it1=<1*D+ -1*H+1,it1=<1*K1+ -1*H+1 with precondition: [G1=0,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,D+1=O1,I=P1,J=Q1,K=R1,L=S1,N=U1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,V1=L2,F1=M2,0>=F+1,H>=1,D>=H] f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[[63],64]: 1+it1*(1) Such that:it1=<1*K1,it1=<1*O1+ -1,it1=<1*D+ -1*H+1,it1=<1*K1+ -1*H+1 with precondition: [G1=0,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,D+1=O1,I=P1,J=Q1,K=R1,L=S1,N=U1,N1=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,N1=L2,F1=M2,F>=0,H>=1,D>=H] f42(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,F2,G2,H2,I2,J2,K2,L2,M2):[[63],65]: 0+it1*(1) Such that:it1=<1*D,it1=<1*K1,it1=<1*O1+ -1,it1=<1*O1+ -1*H,it1=<1*D+ -1*H+1,it1=<1*K1+ -1*H+1 with precondition: [G1=1,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,I=P1,J=Q1,K=R1,L=S1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U=B2,V=C2,W=D2,X=E2,Y=F2,Z=G2,A1=H2,B1=I2,C1=J2,D1=K2,E1=L2,F1=M2,F>=0,H>=1,O1>=H+1,D+1>=O1] Inferred cost of f72(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,F2,G2,H2,I2,J2,K2,L2,M2): f72(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,F2,G2,H2,I2,J2,K2,L2,M2):[[68],69]: 1+it1*(1) Such that:it1=<8,it1=<-1*Y+8 with precondition: [W=0,G1=0,D2=0,F2=8,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,G=N1,H=O1,I=P1,J=Q1,K=R1,L=S1,M=T1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,T=A2,U+1=B2,V=C2,Z=G2,A1=H2,B1=I2,C1=J2,E2=K2,E1=L2,F1=M2,255>=U,7>=Y,Y>=0] Inferred cost of f66(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,F2,G2,H2,I2,J2,K2,L2,M2): f66(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,F2,G2,H2,I2,J2,K2,L2,M2):[[71],72]: 1+it1*(2+it2*(1)) Such that:it1=<256,it1=<-1*U+256 it2=<8 with precondition: [A=1,R=0,S=1,G1=0,H1=1,Y1=0,Z1=1,B2=256,D2=0,F2=8,N=O,N=P,B+2=Q,N=T,B=I1,C=J1,D=K1,E=L1,F=M1,G=N1,H=O1,I=P1,J=Q1,K=R1,L=S1,M=T1,N=U1,N=V1,N=W1,B+2=X1,N=A2,Z=G2,A1=H2,B1=I2,C1=J2,E2=K2,E1=L2,F1=M2,255>=U] Inferred cost of f91(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,F2,G2,H2,I2,J2,K2,L2,M2): f91(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,F2,G2,H2,I2,J2,K2,L2,M2):[76]: 1 with precondition: [U=1,G1=1,B2=1,H1=A,I1=B,J1=C,K1=D,L1=E,M1=F,N1=G,O1=H,P1=I,Q1=J,R1=K,S1=L,T1=M,U1=N,V1=O,W1=P,Y1=R,C2=V,D2=W,E2=X,F2=Y,G2=Z,K2=D1,L2=E1,M2=F1,Q=X1,S=Z1,T=A2,T=H2,T=I2,T=J2,0>=Q,S>=0] f91(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,F2,G2,H2,I2,J2,K2,L2,M2):[77]: 1 with precondition: [U=1,G1=1,B2=1,H1=A,I1=B,J1=C,K1=D,L1=E,M1=F,N1=G,O1=H,P1=I,Q1=J,R1=K,S1=L,T1=M,U1=N,V1=O,W1=P,Y1=R,A2=T,C2=V,D2=W,E2=X,F2=Y,G2=Z,K2=D1,L2=E1,M2=F1,Q=X1,S=Z1,H2=I2,H2=J2,0>=Q,0>=S+1] f91(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,F2,G2,H2,I2,J2,K2,L2,M2):[[74],77]: 1+it1*(1) Such that:it1=<1*X1,it1=<1*B2+ -1,it1=<1*Q+ -1*U+1,it1=<1*X1+ -1*U+1 with precondition: [G1=1,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,G=N1,H=O1,I=P1,J=Q1,K=R1,L=S1,M=T1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,Q+1=B2,V=C2,W=D2,X=E2,Y=F2,H2=I2,H2=J2,D1=K2,E1=L2,F1=M2,0>=S+1,U>=1,Q>=U] f91(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,F2,G2,H2,I2,J2,K2,L2,M2):[[75],76]: 1+it1*(1) Such that:it1=<1*X1,it1=<1*B2+ -1,it1=<1*Q+ -1*U+1,it1=<1*X1+ -1*U+1 with precondition: [G1=1,A=H1,B=I1,C=J1,D=K1,E=L1,F=M1,G=N1,H=O1,I=P1,J=Q1,K=R1,L=S1,M=T1,N=U1,O=V1,P=W1,Q=X1,R=Y1,S=Z1,Q+1=B2,V=C2,W=D2,X=E2,Y=F2,A2=H2,A2=I2,A2=J2,D1=K2,E1=L2,F1=M2,S>=0,U>=1,Q>=U] Inferred cost of f85(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): f85(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):[79]: 2 with precondition: [0>=Q,R>=0,S>=0] f85(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):[80]: 2 with precondition: [0>=Q,0>=S+1,R>=0] f85(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):[81]: 2+it1*(1) Such that:it1=<1*Q with precondition: [0>=S+1,Q>=1,R>=0] f85(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):[82]: 2+it1*(1) Such that:it1=<1*Q with precondition: [Q>=1,R>=0,S>=0] f85(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):[83]: 2 with precondition: [0>=Q,0>=R+1,S>=0] f85(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):[84]: 2+it1*(1) Such that:it1=<1*Q with precondition: [0>=R+1,Q>=1,S>=0] f85(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):[85]: 2 with precondition: [0>=Q,0>=R+1,0>=S+1] f85(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):[86]: 2+it1*(1) Such that:it1=<1*Q with precondition: [0>=R+1,0>=S+1,Q>=1] Inferred cost of loop_cont_f66(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): loop_cont_f66(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):[88]: 2 with precondition: [0>=Q,R>=0,S>=0] loop_cont_f66(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):[89]: 2 with precondition: [0>=Q,0>=S+1,R>=0] loop_cont_f66(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):[90]: 2+it1*(1) Such that:it1=<1*Q with precondition: [0>=S+1,Q>=1,R>=0] loop_cont_f66(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):[91]: 2+it1*(1) Such that:it1=<1*Q with precondition: [Q>=1,R>=0,S>=0] loop_cont_f66(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):[92]: 2 with precondition: [0>=Q,0>=R+1,S>=0] loop_cont_f66(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):[93]: 2+it1*(1) Such that:it1=<1*Q with precondition: [0>=R+1,Q>=1,S>=0] loop_cont_f66(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):[94]: 2 with precondition: [0>=Q,0>=R+1,0>=S+1] loop_cont_f66(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):[95]: 2+it1*(1) Such that:it1=<1*Q with precondition: [0>=R+1,0>=S+1,Q>=1] Inferred cost of f56(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): f56(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):[97]: 3 with precondition: [0>=A+1,0>=B+2] f56(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):[98]: 3+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,B+1>=0] f56(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):[99]: 3 with precondition: [0>=B+2,A>=1] f56(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):[100]: 3+it1*(1) Such that:it1=<1*B+2 with precondition: [A>=1,B+1>=0] f56(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):[101]: 4+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2] f56(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):[102]: 4+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,B+1>=0] Inferred cost of loop_cont_f42(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): loop_cont_f42(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):[104]: 3 with precondition: [0>=A+1,0>=B+2] loop_cont_f42(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):[105]: 3+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,B+1>=0] loop_cont_f42(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):[106]: 3 with precondition: [0>=B+2,A>=1] loop_cont_f42(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):[107]: 3+it1*(1) Such that:it1=<1*B+2 with precondition: [A>=1,B+1>=0] loop_cont_f42(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):[108]: 4+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2] loop_cont_f42(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):[109]: 4+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,B+1>=0] Inferred cost of f36(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): f36(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):[111]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,E>=0,F>=0] f36(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):[112]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,B+1>=0,E>=0,F>=0] f36(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):[113]: 5 with precondition: [0>=B+2,0>=D,A>=1,E>=0,F>=0] f36(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):[114]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,A>=1,B+1>=0,E>=0,F>=0] f36(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):[115]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,E>=0,F>=0] f36(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):[116]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,B+1>=0,E>=0,F>=0] f36(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):[117]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,0>=F+1,E>=0] f36(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):[118]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,0>=F+1,B+1>=0,E>=0] f36(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):[119]: 5 with precondition: [0>=B+2,0>=D,0>=F+1,A>=1,E>=0] f36(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):[120]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,0>=F+1,A>=1,B+1>=0,E>=0] f36(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):[121]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,0>=F+1,E>=0] f36(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):[122]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,0>=F+1,B+1>=0,E>=0] f36(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):[123]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,0>=F+1,D>=1,E>=0] f36(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):[124]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,0>=F+1,B+1>=0,D>=1,E>=0] f36(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):[125]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,0>=F+1,A>=1,D>=1,E>=0] f36(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):[126]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=F+1,A>=1,B+1>=0,D>=1,E>=0] f36(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):[127]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,0>=F+1,D>=1,E>=0] f36(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):[128]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,0>=F+1,B+1>=0,D>=1,E>=0] f36(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):[129]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,D>=1,E>=0,F>=0] f36(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):[130]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,B+1>=0,D>=1,E>=0,F>=0] f36(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):[131]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,A>=1,D>=1,E>=0,F>=0] f36(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):[132]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [A>=1,B+1>=0,D>=1,E>=0,F>=0] f36(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):[133]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,D>=1,E>=0,F>=0] f36(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):[134]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,B+1>=0,D>=1,E>=0,F>=0] f36(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):[135]: 1 with precondition: [E>=0] f36(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):[136]: 1+it1*(1) Such that:it1=<1*D with precondition: [0>=F+1,D>=1,E>=0] f36(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):[137]: 1+it1*(1) Such that:it1=<1*D with precondition: [D>=1,E>=0,F>=0] f36(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):[138]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,0>=E+1,F>=0] f36(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):[139]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,0>=E+1,B+1>=0,F>=0] f36(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):[140]: 5 with precondition: [0>=B+2,0>=D,0>=E+1,A>=1,F>=0] f36(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):[141]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,0>=E+1,A>=1,B+1>=0,F>=0] f36(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):[142]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,0>=E+1,F>=0] f36(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):[143]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,0>=E+1,B+1>=0,F>=0] f36(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):[144]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,0>=E+1,D>=1,F>=0] f36(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):[145]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,0>=E+1,B+1>=0,D>=1,F>=0] f36(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):[146]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,0>=E+1,A>=1,D>=1,F>=0] f36(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):[147]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=E+1,A>=1,B+1>=0,D>=1,F>=0] f36(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):[148]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,0>=E+1,D>=1,F>=0] f36(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):[149]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,0>=E+1,B+1>=0,D>=1,F>=0] f36(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):[150]: 1 with precondition: [0>=E+1,F>=0] f36(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):[151]: 1+it1*(1) Such that:it1=<1*D with precondition: [0>=E+1,D>=1,F>=0] f36(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):[152]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,0>=E+1,0>=F+1] f36(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):[153]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,0>=E+1,0>=F+1,B+1>=0] f36(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):[154]: 5 with precondition: [0>=B+2,0>=D,0>=E+1,0>=F+1,A>=1] f36(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):[155]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,0>=E+1,0>=F+1,A>=1,B+1>=0] f36(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):[156]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,0>=E+1,0>=F+1] f36(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):[157]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,0>=E+1,0>=F+1,B+1>=0] f36(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):[158]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,0>=E+1,0>=F+1,D>=1] f36(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):[159]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,0>=E+1,0>=F+1,B+1>=0,D>=1] f36(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):[160]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,0>=E+1,0>=F+1,A>=1,D>=1] f36(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):[161]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=E+1,0>=F+1,A>=1,B+1>=0,D>=1] f36(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):[162]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,0>=E+1,0>=F+1,D>=1] f36(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):[163]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,0>=E+1,0>=F+1,B+1>=0,D>=1] f36(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):[164]: 1 with precondition: [0>=E+1,0>=F+1] f36(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):[165]: 1+it1*(1) Such that:it1=<1*D with precondition: [0>=E+1,0>=F+1,D>=1] Inferred cost of loop_cont_f17(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): loop_cont_f17(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):[167]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,E>=0,F>=0] loop_cont_f17(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):[168]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,B+1>=0,E>=0,F>=0] loop_cont_f17(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):[169]: 5 with precondition: [0>=B+2,0>=D,A>=1,E>=0,F>=0] loop_cont_f17(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):[170]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,A>=1,B+1>=0,E>=0,F>=0] loop_cont_f17(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):[171]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,E>=0,F>=0] loop_cont_f17(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):[172]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,B+1>=0,E>=0,F>=0] loop_cont_f17(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):[173]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,0>=F+1,E>=0] loop_cont_f17(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):[174]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,0>=F+1,B+1>=0,E>=0] loop_cont_f17(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):[175]: 5 with precondition: [0>=B+2,0>=D,0>=F+1,A>=1,E>=0] loop_cont_f17(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):[176]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,0>=F+1,A>=1,B+1>=0,E>=0] loop_cont_f17(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):[177]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,0>=F+1,E>=0] loop_cont_f17(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):[178]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,0>=F+1,B+1>=0,E>=0] loop_cont_f17(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):[179]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,0>=F+1,D>=1,E>=0] loop_cont_f17(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):[180]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,0>=F+1,B+1>=0,D>=1,E>=0] loop_cont_f17(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):[181]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,0>=F+1,A>=1,D>=1,E>=0] loop_cont_f17(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):[182]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=F+1,A>=1,B+1>=0,D>=1,E>=0] loop_cont_f17(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):[183]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,0>=F+1,D>=1,E>=0] loop_cont_f17(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):[184]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,0>=F+1,B+1>=0,D>=1,E>=0] loop_cont_f17(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):[185]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,D>=1,E>=0,F>=0] loop_cont_f17(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):[186]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,B+1>=0,D>=1,E>=0,F>=0] loop_cont_f17(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):[187]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,A>=1,D>=1,E>=0,F>=0] loop_cont_f17(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):[188]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [A>=1,B+1>=0,D>=1,E>=0,F>=0] loop_cont_f17(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):[189]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,D>=1,E>=0,F>=0] loop_cont_f17(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):[190]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,B+1>=0,D>=1,E>=0,F>=0] loop_cont_f17(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):[191]: 1 with precondition: [E>=0] loop_cont_f17(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):[192]: 1+it1*(1) Such that:it1=<1*D with precondition: [0>=F+1,D>=1,E>=0] loop_cont_f17(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):[193]: 1+it1*(1) Such that:it1=<1*D with precondition: [D>=1,E>=0,F>=0] loop_cont_f17(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):[194]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,0>=E+1,F>=0] loop_cont_f17(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):[195]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,0>=E+1,B+1>=0,F>=0] loop_cont_f17(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):[196]: 5 with precondition: [0>=B+2,0>=D,0>=E+1,A>=1,F>=0] loop_cont_f17(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):[197]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,0>=E+1,A>=1,B+1>=0,F>=0] loop_cont_f17(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):[198]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,0>=E+1,F>=0] loop_cont_f17(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):[199]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,0>=E+1,B+1>=0,F>=0] loop_cont_f17(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):[200]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,0>=E+1,D>=1,F>=0] loop_cont_f17(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):[201]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,0>=E+1,B+1>=0,D>=1,F>=0] loop_cont_f17(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):[202]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,0>=E+1,A>=1,D>=1,F>=0] loop_cont_f17(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):[203]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=E+1,A>=1,B+1>=0,D>=1,F>=0] loop_cont_f17(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):[204]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,0>=E+1,D>=1,F>=0] loop_cont_f17(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):[205]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,0>=E+1,B+1>=0,D>=1,F>=0] loop_cont_f17(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):[206]: 1 with precondition: [0>=E+1,F>=0] loop_cont_f17(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):[207]: 1+it1*(1) Such that:it1=<1*D with precondition: [0>=E+1,D>=1,F>=0] loop_cont_f17(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):[208]: 5 with precondition: [0>=A+1,0>=B+2,0>=D,0>=E+1,0>=F+1] loop_cont_f17(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):[209]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=A+1,0>=D,0>=E+1,0>=F+1,B+1>=0] loop_cont_f17(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):[210]: 5 with precondition: [0>=B+2,0>=D,0>=E+1,0>=F+1,A>=1] loop_cont_f17(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):[211]: 5+it1*(1) Such that:it1=<1*B+2 with precondition: [0>=D,0>=E+1,0>=F+1,A>=1,B+1>=0] loop_cont_f17(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):[212]: 6+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0,0>=B+2,0>=D,0>=E+1,0>=F+1] loop_cont_f17(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):[213]: 6+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<1*B+2 it2=<8 with precondition: [A=0,0>=D,0>=E+1,0>=F+1,B+1>=0] loop_cont_f17(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):[214]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=A+1,0>=B+2,0>=E+1,0>=F+1,D>=1] loop_cont_f17(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):[215]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=A+1,0>=E+1,0>=F+1,B+1>=0,D>=1] loop_cont_f17(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):[216]: 5+it1*(1) Such that:it1=<1*D with precondition: [0>=B+2,0>=E+1,0>=F+1,A>=1,D>=1] loop_cont_f17(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):[217]: 5+it1*(1)+it2*(1) Such that:it1=<1*D,it2=<1*B+2 with precondition: [0>=E+1,0>=F+1,A>=1,B+1>=0,D>=1] loop_cont_f17(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):[218]: 6+it1*(1)+it2*(2+it3*(1)) Such that:it1=<1*D,it2=<256 it3=<8 with precondition: [A=0,0>=B+2,0>=E+1,0>=F+1,D>=1] loop_cont_f17(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):[219]: 6+it1*(1)+it2*(2+it3*(1))+it4*(1) Such that:it1=<1*D,it2=<256,it4=<1*B+2 it3=<8 with precondition: [A=0,0>=E+1,0>=F+1,B+1>=0,D>=1] loop_cont_f17(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):[220]: 1 with precondition: [0>=E+1,0>=F+1] loop_cont_f17(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):[221]: 1+it1*(1) Such that:it1=<1*D with precondition: [0>=E+1,0>=F+1,D>=1] 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,W,X,Y,Z,A1,B1,C1,D1,E1,F1): f0(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):[223]: 6+it1*(1)+it2*(1) Such that:it1=<40,it2=<42 with precondition: [0>=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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[224]: 2 with precondition: [0>=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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[225]: 2+it1*(1) Such that:it1=<40 with precondition: [0>=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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[226]: 6+it1*(1)+it2*(1) Such that:it1=<40,it2=<42 with precondition: [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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[227]: 2 with precondition: [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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[228]: 2+it1*(1) Such that:it1=<40 with precondition: [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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[229]: 7+it1*(2+it2*(1))+it3*(1)+it4*(1) Such that:it1=<256,it3=<40,it4=<42 it2=<8 with precondition: [A=0] f0(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):[230]: 3+it1*(2+it2*(1)) Such that:it1=<256 it2=<8 with precondition: [A=0] f0(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):[231]: 3+it1*(2+it2*(1))+it3*(1) Such that:it1=<256,it3=<40 it2=<8 with precondition: [A=0] 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,W,X,Y,Z,A1,B1,C1,D1,E1,F1): f0(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):[223]: 88 with precondition: [0>=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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[224]: 2 with precondition: [0>=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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[225]: 42 with precondition: [0>=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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[226]: 88 with precondition: [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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[227]: 2 with precondition: [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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[228]: 42 with precondition: [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,W,X,Y,Z,A1,B1,C1,D1,E1,F1):[229]: 2649 with precondition: [A=0] f0(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):[230]: 2563 with precondition: [A=0] f0(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):[231]: 2603 with precondition: [A=0] 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,W,X,Y,Z,A1,B1,C1,D1,E1,F1): 2649 Asymptotic class: constant Time statistics: Partial evaluation computed in 368 ms. Invariants computed in 1062 ms. ----Backward Invariants 439 ms. ----Transitive Invariants 234 ms. Refinement performed in 1868 ms. Termination proved in 743 ms. Upper bounds computed in 949 ms. ----Phase cost structures 635 ms. --------Equation cost structures 619 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 272 ms. ----Solving cost expressions 1 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 5832 ms.