warning: Ignored call to f57/21 in equation f54/21 warning: Ignored call to loop_cont_f52/21 in equation f45/21 warning: Ignored call to loop_cont_f52/21 in equation f45/21 Warning: the following predicates are never called:[f54/21] Inferred cost of f13(A,B,C,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): f13(A,B,C,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):[30]: 1 with precondition: [F=0,U=0,V=0,B1=0,Q1=0,Y=C,Z=D,A1=E,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,A=W,B=X,A>=B] f13(A,B,C,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):[31]: 0 with precondition: [F=0,U=0,V=1,B1=0,Q1=0,Y=C,Z=D,A1=E,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,A=W,B=X,B>=A+1] f13(A,B,C,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):[32]: 1 with precondition: [F=0,U=0,V=0,B1=0,Q1=0,Y=C,Z=D,C1=G,K1=O,L1=P,M1=Q,N1=R,O1=S,P1=T,A=W,B=X,E=A1,E=H1,D1=I1,D1=J1,D1>=1,B>=A+1] f13(A,B,C,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):[33]: 0 with precondition: [F=0,U=0,V=1,B1=0,Q1=0,W=A,X=B,Y=C,Z=D,A1=E,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] f13(A,B,C,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):[34]: 1 with precondition: [F=0,U=0,V=0,B1=0,M1=0,P1=0,Q1=0,Z=D,C1=G,L1=Q,A=W,B=X,E=A1,E=H1,D1=I1,D1=J1,D1=K1,Y=N1,Y=O1,0>=D1,Y>=2,B>=A+1] f13(A,B,C,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):[35]: 1 with precondition: [F=0,U=0,V=0,B1=0,M1=0,P1=0,Q1=0,Z=D,C1=G,L1=Q,A=W,B=X,E=A1,E=H1,D1=I1,D1=J1,D1=K1,Y=N1,Y=O1,0>=Y,0>=D1,B>=A+1] f13(A,B,C,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):[[29],30]: 1+it1*(1) Such that:it1=<1*W+ -1*A,it1=<1*X+ -1*A with precondition: [F=0,U=0,V=0,Y=1,B1=0,N1=1,O1=1,P1=0,Q1=0,B=W,B=X,D=Z,E=A1,G=C1,E=H1,D1=I1,D1=J1,D1=K1,Q=L1,Q=M1,0>=D1,B>=A+1] f13(A,B,C,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):[[29],31]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*W+ -1*A with precondition: [F=0,U=0,V=1,Y=1,B1=0,N1=1,O1=1,P1=0,Q1=0,B=X,D=Z,E=A1,G=C1,E=H1,D1=I1,D1=J1,D1=K1,Q=L1,Q=M1,0>=D1,W>=A+1,B>=W+1] f13(A,B,C,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):[[29],32]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*W+ -1*A with precondition: [F=0,U=0,V=0,Y=1,B1=0,N1=1,O1=1,P1=0,Q1=0,B=X,D=Z,E=A1,G=C1,E=H1,D1=I1,D1=J1,Q=L1,Q=M1,0>=K1,D1>=1,W>=A+1,B>=W+1] f13(A,B,C,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):[[29],33]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*W+ -1*A with precondition: [F=0,U=0,V=1,Y=1,B1=0,N1=1,O1=1,P1=0,Q1=0,B=X,D=Z,E=A1,G=C1,E=H1,D1=I1,D1=J1,D1=K1,Q=L1,Q=M1,0>=D1,W>=A+1,B>=W] f13(A,B,C,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):[[29],34]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*W+ -1*A with precondition: [F=0,U=0,V=0,B1=0,M1=0,P1=0,Q1=0,B=X,D=Z,E=A1,G=C1,E=H1,D1=I1,D1=J1,D1=K1,Q=L1,Y=N1,Y=O1,0>=D1,Y>=2,W>=A+1,B>=W+1] f13(A,B,C,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):[[29],35]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*W+ -1*A with precondition: [F=0,U=0,V=0,B1=0,M1=0,P1=0,Q1=0,B=X,D=Z,E=A1,G=C1,E=H1,D1=I1,D1=J1,D1=K1,Q=L1,Y=N1,Y=O1,0>=Y,0>=D1,W>=A+1,B>=W+1] Inferred cost of f52(A,B,C,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): f52(A,B,C,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):[38]: 0 with precondition: [E=0,V=1,A1=0,W=A,X=B,Y=C,Z=D,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] f52(A,B,C,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):[[37],38]: inf with precondition: [E=0,V=1,A1=0,A=W,B=X,C=Y,D=Z,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=P1,U=Q1] f52(A,B,C,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):[[37],39]...: inf with precondition: [E=0,1>=V,V>=0] Inferred cost of f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[40]: 1 with precondition: [D>=1] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[41]: inf with precondition: [D>=1] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[42]: 1 with precondition: [0>=D] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[43]: inf with precondition: [0>=D] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[44]...: inf with precondition: [D>=1] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[45]...: inf with precondition: [D>=1] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[46]...: inf with precondition: [0>=D] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[47]...: inf with precondition: [0>=D] 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): f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[49]: 2 with precondition: [C>=3,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[50]: inf with precondition: [C>=3,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[51]: 2 with precondition: [0>=D,C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[52]: inf with precondition: [0>=D,C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[53]: 2 with precondition: [1>=C,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[54]: inf with precondition: [1>=C,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[55]: 2 with precondition: [1>=C,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[56]: inf with precondition: [1>=C,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[57]: 2 with precondition: [C=2,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[58]: inf with precondition: [C=2,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[59]: 2 with precondition: [C=2,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[60]: inf with precondition: [C=2,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[61]...: inf with precondition: [C>=3,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[62]...: inf with precondition: [C>=3,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[63]...: inf with precondition: [0>=D,C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[64]...: inf with precondition: [0>=D,C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[65]...: inf with precondition: [1>=C,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[66]...: inf with precondition: [1>=C,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[67]...: inf with precondition: [1>=C,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[68]...: inf with precondition: [1>=C,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[69]...: inf with precondition: [C=2,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[70]...: inf with precondition: [C=2,D>=1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[71]...: inf with precondition: [C=2,0>=D] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[72]...: inf with precondition: [C=2,0>=D] Inferred cost of loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[74]: 1 with precondition: [D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[75]: inf with precondition: [D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[76]: 1 with precondition: [0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[77]: inf with precondition: [0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[78]: 2 with precondition: [C>=3,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[79]: inf with precondition: [C>=3,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[80]: 2 with precondition: [0>=D,C>=3] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[81]: inf with precondition: [0>=D,C>=3] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[82]: 2 with precondition: [1>=C,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[83]: inf with precondition: [1>=C,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[84]: 2 with precondition: [1>=C,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[85]: inf with precondition: [1>=C,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[86]: 2 with precondition: [C=2,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[87]: inf with precondition: [C=2,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[88]: 2 with precondition: [C=2,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[89]: inf with precondition: [C=2,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[90]...: inf with precondition: [D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[91]...: inf with precondition: [D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[92]...: inf with precondition: [0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[93]...: inf with precondition: [0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[94]...: inf with precondition: [C>=3,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[95]...: inf with precondition: [C>=3,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[96]...: inf with precondition: [0>=D,C>=3] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[97]...: inf with precondition: [0>=D,C>=3] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[98]...: inf with precondition: [1>=C,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[99]...: inf with precondition: [1>=C,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[100]...: inf with precondition: [1>=C,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[101]...: inf with precondition: [1>=C,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[102]...: inf with precondition: [C=2,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[103]...: inf with precondition: [C=2,D>=1] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[104]...: inf with precondition: [C=2,0>=D] loop_cont_f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[105]...: inf with precondition: [C=2,0>=D] 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): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[107]: 3 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):[108]: 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):[109]: 4 with precondition: [C>=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):[110]: inf with precondition: [C>=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):[111]: 4 with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[112]: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[113]: 4 with precondition: [C=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):[114]: inf with precondition: [C=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):[115]: 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):[116]: 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):[117]: 4 with precondition: [C>=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):[118]: inf with precondition: [C>=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):[119]: 4 with precondition: [1>=C,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):[120]: inf with precondition: [1>=C,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):[121]: 4 with precondition: [C=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):[122]: inf with precondition: [C=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):[123]: 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):[124]: 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):[125]: 4 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):[126]: 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):[127]: 4 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):[128]: 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):[129]: 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):[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):[131]: 4 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):[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):[133]: 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):[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):[135]: 4+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):[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):[137]: 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):[138]: 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):[139]: 4+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):[140]: 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):[141]: 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):[142]: 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):[143]: 4+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):[144]: 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):[145]: 4+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):[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):[147]: 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):[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):[149]: 4+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):[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):[151]: 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):[152]: 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):[153]: 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):[154]: 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):[155]: 3 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):[156]: 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):[157]: 4 with precondition: [C>=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):[158]: inf with precondition: [C>=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):[159]: 4 with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[160]: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[161]: 4 with precondition: [C=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):[162]: inf with precondition: [C=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):[163]: 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):[164]: 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):[165]: 4 with precondition: [C>=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):[166]: inf with precondition: [C>=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):[167]: 4 with precondition: [1>=C,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):[168]: inf with precondition: [1>=C,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):[169]: 4 with precondition: [C=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):[170]: inf with precondition: [C=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):[171]: 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):[172]: 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):[173]: 4 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):[174]: 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):[175]: 4 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):[176]: 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):[177]: 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):[178]: 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):[179]: 4 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):[180]: 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):[181]: 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):[182]: 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):[183]: 4+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):[184]: 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):[185]: 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):[186]: 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):[187]: 4+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):[188]: 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):[189]: 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):[190]: 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):[191]: 4+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):[192]: 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):[193]: 4+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):[194]: 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):[195]: 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):[196]: 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):[197]: 4+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):[198]: 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):[199]: 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):[200]: 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):[201]: 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):[202]: 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):[203]...: 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):[204]...: 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):[205]...: inf with precondition: [C>=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):[206]...: inf with precondition: [C>=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):[207]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[208]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[209]...: inf with precondition: [C=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):[210]...: inf with precondition: [C=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):[211]...: 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):[212]...: 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):[213]...: inf with precondition: [C>=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):[214]...: inf with precondition: [C>=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):[215]...: inf with precondition: [1>=C,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):[216]...: inf with precondition: [1>=C,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):[217]...: inf with precondition: [C=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):[218]...: inf with precondition: [C=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):[219]...: 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):[220]...: 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):[221]...: 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):[222]...: 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):[223]...: 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):[224]...: 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):[225]...: 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):[226]...: 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):[227]...: 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):[228]...: 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):[229]...: 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):[230]...: 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):[231]...: 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):[232]...: 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):[233]...: 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):[234]...: 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):[235]...: 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):[236]...: 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):[237]...: 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):[238]...: 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):[239]...: 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):[240]...: 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):[241]...: 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):[242]...: 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):[243]...: 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):[244]...: 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):[245]...: 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):[246]...: 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):[247]...: 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):[248]...: 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):[249]...: inf with precondition: [C>=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):[250]...: inf with precondition: [C>=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):[251]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[252]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[253]...: inf with precondition: [C=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):[254]...: inf with precondition: [C=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):[255]...: 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):[256]...: 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):[257]...: inf with precondition: [C>=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):[258]...: inf with precondition: [C>=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):[259]...: inf with precondition: [1>=C,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):[260]...: inf with precondition: [1>=C,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):[261]...: inf with precondition: [C=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):[262]...: inf with precondition: [C=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):[263]...: 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):[264]...: 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):[265]...: 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):[266]...: 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):[267]...: 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):[268]...: 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):[269]...: 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):[270]...: 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):[271]...: 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):[272]...: 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):[273]...: 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):[274]...: 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):[275]...: 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):[276]...: 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):[277]...: 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):[278]...: 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):[279]...: 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):[280]...: 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):[281]...: 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):[282]...: 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):[283]...: 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):[284]...: 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):[285]...: 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):[286]...: 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):[287]...: 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):[288]...: 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):[289]...: 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):[290]...: 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): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[107]: 3 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):[108]: 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):[109]: 4 with precondition: [C>=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):[110]: inf with precondition: [C>=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):[111]: 4 with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[112]: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[113]: 4 with precondition: [C=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):[114]: inf with precondition: [C=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):[115]: 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):[116]: 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):[117]: 4 with precondition: [C>=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):[118]: inf with precondition: [C>=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):[119]: 4 with precondition: [1>=C,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):[120]: inf with precondition: [1>=C,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):[121]: 4 with precondition: [C=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):[122]: inf with precondition: [C=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):[123]: 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):[124]: 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):[125]: 4 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):[126]: 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):[127]: 4 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):[128]: 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):[129]: 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):[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):[131]: 4 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):[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):[133]: -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):[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):[135]: -1*A+1*B+4 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):[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):[137]: -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):[138]: 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):[139]: -1*A+1*B+3 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):[140]: 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):[141]: -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):[142]: 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):[143]: -1*A+1*B+3 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):[144]: 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):[145]: -1*A+1*B+3 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):[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):[147]: -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):[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):[149]: -1*A+1*B+3 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):[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):[151]: 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):[152]: 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):[153]: -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):[154]: -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):[155]: 3 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):[156]: 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):[157]: 4 with precondition: [C>=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):[158]: inf with precondition: [C>=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):[159]: 4 with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[160]: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[161]: 4 with precondition: [C=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):[162]: inf with precondition: [C=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):[163]: 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):[164]: 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):[165]: 4 with precondition: [C>=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):[166]: inf with precondition: [C>=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):[167]: 4 with precondition: [1>=C,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):[168]: inf with precondition: [1>=C,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):[169]: 4 with precondition: [C=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):[170]: inf with precondition: [C=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):[171]: 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):[172]: 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):[173]: 4 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):[174]: 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):[175]: 4 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):[176]: 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):[177]: 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):[178]: 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):[179]: 4 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):[180]: 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):[181]: -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):[182]: 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):[183]: -1*A+1*B+4 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):[184]: 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):[185]: -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):[186]: 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):[187]: -1*A+1*B+3 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):[188]: 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):[189]: -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):[190]: 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):[191]: -1*A+1*B+3 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):[192]: 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):[193]: -1*A+1*B+3 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):[194]: 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):[195]: -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):[196]: 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):[197]: -1*A+1*B+3 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):[198]: 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):[199]: 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):[200]: 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):[201]: -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):[202]: -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):[203]...: 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):[204]...: 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):[205]...: inf with precondition: [C>=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):[206]...: inf with precondition: [C>=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):[207]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[208]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[209]...: inf with precondition: [C=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):[210]...: inf with precondition: [C=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):[211]...: 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):[212]...: 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):[213]...: inf with precondition: [C>=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):[214]...: inf with precondition: [C>=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):[215]...: inf with precondition: [1>=C,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):[216]...: inf with precondition: [1>=C,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):[217]...: inf with precondition: [C=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):[218]...: inf with precondition: [C=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):[219]...: 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):[220]...: 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):[221]...: 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):[222]...: 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):[223]...: 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):[224]...: 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):[225]...: 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):[226]...: 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):[227]...: 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):[228]...: 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):[229]...: 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):[230]...: 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):[231]...: 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):[232]...: 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):[233]...: 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):[234]...: 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):[235]...: 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):[236]...: 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):[237]...: 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):[238]...: 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):[239]...: 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):[240]...: 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):[241]...: 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):[242]...: 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):[243]...: 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):[244]...: 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):[245]...: 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):[246]...: 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):[247]...: 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):[248]...: 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):[249]...: inf with precondition: [C>=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):[250]...: inf with precondition: [C>=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):[251]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[252]...: inf with precondition: [1>=C,A>=B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[253]...: inf with precondition: [C=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):[254]...: inf with precondition: [C=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):[255]...: 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):[256]...: 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):[257]...: inf with precondition: [C>=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):[258]...: inf with precondition: [C>=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):[259]...: inf with precondition: [1>=C,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):[260]...: inf with precondition: [1>=C,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):[261]...: inf with precondition: [C=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):[262]...: inf with precondition: [C=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):[263]...: 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):[264]...: 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):[265]...: 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):[266]...: 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):[267]...: 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):[268]...: 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):[269]...: 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):[270]...: 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):[271]...: 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):[272]...: 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):[273]...: 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):[274]...: 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):[275]...: 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):[276]...: 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):[277]...: 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):[278]...: 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):[279]...: 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):[280]...: 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):[281]...: 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):[282]...: 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):[283]...: 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):[284]...: 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):[285]...: 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):[286]...: 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):[287]...: 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):[288]...: 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):[289]...: 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):[290]...: 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): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 72 ms. Invariants computed in 304 ms. ----Backward Invariants 193 ms. ----Transitive Invariants 29 ms. Refinement performed in 1137 ms. Termination proved in 69 ms. Upper bounds computed in 744 ms. ----Phase cost structures 523 ms. --------Equation cost structures 507 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 146 ms. ----Solving cost expressions 10 ms. Compressed phase information: 12 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 2479 ms.