warning: Ignored call to f58/23 in equation f55/23 warning: Ignored call to loop_cont_f53/23 in equation f45/23 warning: Ignored call to loop_cont_f53/23 in equation f45/23 Warning: the following predicates are never called:[f55/23] 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,T1,U1): 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,T1,U1):[28]: 1 with precondition: [F=0,W=0,X=0,D1=0,U1=0,A1=C,B1=D,C1=E,E1=G,F1=H,G1=I,H1=J,I1=K,J1=L,K1=M,L1=N,M1=O,N1=P,O1=Q,P1=R,Q1=S,R1=T,S1=U,T1=V,A=Y,B=Z,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,T1,U1):[29]: 0 with precondition: [F=0,W=0,X=1,D1=0,U1=0,A1=C,B1=D,C1=E,E1=G,F1=H,G1=I,H1=J,I1=K,J1=L,K1=M,L1=N,M1=O,N1=P,O1=Q,P1=R,Q1=S,R1=T,S1=U,T1=V,A=Y,B=Z,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,T1,U1):[30]: 1 with precondition: [F=0,W=0,X=0,D1=0,U1=0,A1=C,C1=E,E1=G,N1=P,O1=Q,P1=R,Q1=S,R1=T,S1=U,T1=V,A=Y,B=Z,D=B1,D=J1,F1=K1,F1=L1,F1=M1,F1>=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,T1,U1):[31]: 0 with precondition: [F=0,W=0,X=1,D1=0,U1=0,Y=A,Z=B,A1=C,B1=D,C1=E,E1=G,F1=H,G1=I,H1=J,I1=K,J1=L,K1=M,L1=N,M1=O,N1=P,O1=Q,P1=R,Q1=S,R1=T,S1=U,T1=V] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1):[32]: 1 with precondition: [F=0,W=0,X=0,D1=0,P1=0,T1=0,U1=0,C1=E,E1=G,O1=R,A=Y,B=Z,D=B1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,A1=Q1,A1=R1,A1=S1,0>=F1,A1>=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,T1,U1):[33]: 1 with precondition: [F=0,W=0,X=0,D1=0,P1=0,T1=0,U1=0,C1=E,E1=G,O1=R,A=Y,B=Z,D=B1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,A1=Q1,A1=R1,A1=S1,0>=A1,0>=F1,B>=A+1] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1):[[27],28]: 1+it1*(1) Such that:it1=<1*Y+ -1*A,it1=<1*Z+ -1*A with precondition: [F=0,W=0,X=0,A1=1,D1=0,Q1=1,R1=1,S1=1,T1=0,U1=0,B=Y,B=Z,D=B1,E=C1,G=E1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,R=O1,R=P1,0>=F1,B>=A+1] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1):[[27],29]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*Y+ -1*A with precondition: [F=0,W=0,X=1,A1=1,D1=0,Q1=1,R1=1,S1=1,T1=0,U1=0,B=Z,D=B1,E=C1,G=E1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,R=O1,R=P1,0>=F1,Y>=A+1,B>=Y+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,T1,U1):[[27],30]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*Y+ -1*A with precondition: [F=0,W=0,X=0,A1=1,D1=0,Q1=1,R1=1,S1=1,T1=0,U1=0,B=Z,D=B1,E=C1,G=E1,D=J1,F1=K1,F1=L1,F1=M1,R=O1,R=P1,0>=N1,F1>=1,Y>=A+1,B>=Y+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,T1,U1):[[27],31]: 0+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*Y+ -1*A with precondition: [F=0,W=0,X=1,A1=1,D1=0,Q1=1,R1=1,S1=1,T1=0,U1=0,B=Z,D=B1,E=C1,G=E1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,R=O1,R=P1,0>=F1,Y>=A+1,B>=Y] 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,T1,U1):[[27],32]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*Y+ -1*A with precondition: [F=0,W=0,X=0,D1=0,P1=0,T1=0,U1=0,B=Z,D=B1,E=C1,G=E1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,R=O1,A1=Q1,A1=R1,A1=S1,0>=F1,A1>=2,Y>=A+1,B>=Y+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,T1,U1):[[27],33]: 1+it1*(1) Such that:it1=<1*B+ -1*A,it1=<1*Y+ -1*A with precondition: [F=0,W=0,X=0,D1=0,P1=0,T1=0,U1=0,B=Z,D=B1,E=C1,G=E1,D=J1,F1=K1,F1=L1,F1=M1,F1=N1,R=O1,A1=Q1,A1=R1,A1=S1,0>=A1,0>=F1,Y>=A+1,B>=Y+1] Inferred cost of f53(A,B,C,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): f53(A,B,C,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):[36]: 0 with precondition: [D=0,X=1,B1=0,Y=A,Z=B,A1=C,C1=E,D1=F,E1=G,F1=H,G1=I,H1=J,I1=K,J1=L,K1=M,L1=N,M1=O,N1=P,O1=Q,P1=R,Q1=S,R1=T,S1=U,T1=V,U1=W] f53(A,B,C,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):[[35],36]: inf with precondition: [D=0,X=1,B1=0,A=Y,B=Z,C=A1,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=T1,W=U1] f53(A,B,C,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):[[35],37]...: inf with precondition: [D=0,1>=X,X>=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,V,W): f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[38]: 1 with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[39]: inf with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[40]: 1 with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[41]: inf with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[42]...: inf with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[43]...: inf with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[44]...: inf with precondition: [] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[45]...: inf with precondition: [] 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,W): f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[47]: 2 with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[48]: inf with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[49]: 2 with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[50]: inf with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[51]: 2 with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[52]: inf with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[53]: 2 with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[54]: inf with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[55]: 2 with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[56]: inf with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[57]: 2 with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[58]: inf with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[59]...: inf with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[60]...: inf with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[61]...: inf with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[62]...: inf with precondition: [C>=3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[63]...: inf with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[64]...: inf with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[65]...: inf with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[66]...: inf with precondition: [1>=C] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[67]...: inf with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[68]...: inf with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[69]...: inf with precondition: [C=2] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[70]...: inf with precondition: [C=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,W): 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,W):[72]: 1 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,W):[73]: 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,W):[74]: 1 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,W):[75]: 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,W):[76]: 2 with precondition: [C>=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,W):[77]: inf with precondition: [C>=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,W):[78]: 2 with precondition: [C>=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,W):[79]: inf with precondition: [C>=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,W):[80]: 2 with precondition: [1>=C] 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,W):[81]: inf with precondition: [1>=C] 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,W):[82]: 2 with precondition: [1>=C] 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,W):[83]: inf with precondition: [1>=C] 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,W):[84]: 2 with precondition: [C=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,W):[85]: inf with precondition: [C=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,W):[86]: 2 with precondition: [C=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,W):[87]: inf with precondition: [C=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,W):[88]...: 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,W):[89]...: 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,W):[90]...: 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,W):[91]...: 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,W):[92]...: inf with precondition: [C>=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,W):[93]...: inf with precondition: [C>=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,W):[94]...: inf with precondition: [C>=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,W):[95]...: inf with precondition: [C>=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,W):[96]...: inf with precondition: [1>=C] 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,W):[97]...: inf with precondition: [1>=C] 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,W):[98]...: inf with precondition: [1>=C] 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,W):[99]...: inf with precondition: [1>=C] 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,W):[100]...: inf with precondition: [C=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,W):[101]...: inf with precondition: [C=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,W):[102]...: inf with precondition: [C=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,W):[103]...: inf with precondition: [C=2] 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): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[105]: 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,V,W):[106]: 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,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[111]: 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,V,W):[112]: 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,V,W):[113]: 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,V,W):[114]: 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,V,W):[115]: 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,V,W):[116]: 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,V,W):[117]: 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,V,W):[118]: 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,V,W):[119]: 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,V,W):[120]: 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,V,W):[121]: 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,W):[122]: 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,W):[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,V,W):[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,V,W):[125]: 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,V,W):[126]: 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,V,W):[127]: 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,V,W):[128]: 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,V,W):[129]: 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,V,W):[130]: 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,V,W):[131]: 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,V,W):[132]: 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,V,W):[133]: 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,V,W):[134]: 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,V,W):[135]: 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,V,W):[136]: 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,V,W):[137]: 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,W):[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,W):[139]: 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,W):[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,W):[141]: 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,V,W):[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,W):[143]: 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,V,W):[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,W):[145]: 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,V,W):[146]: 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,W):[147]: 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,V,W):[148]: 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,W):[149]: 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,W):[150]: 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,W):[151]: 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,W):[152]: 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,W):[153]: 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,V,W):[154]: 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,W):[155]: 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,V,W):[156]: 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,W):[157]: 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,W):[158]: 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,W):[159]: 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,W):[160]: 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,W):[161]: 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,V,W):[162]: 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,W):[163]: 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,V,W):[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,V,W):[165]: 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,W):[166]: 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,W):[167]: 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,W):[168]: 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,W):[169]: 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,V,W):[170]: 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,W):[171]: 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,V,W):[172]: 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,W):[173]: 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,W):[174]: 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,W):[175]: 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,W):[176]: 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,W):[177]: 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,V,W):[178]: 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,W):[179]: 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,V,W):[180]: 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,W):[181]: 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,V,W):[182]: 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,W):[183]: 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,V,W):[184]: 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,W):[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,V,W):[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,V,W):[187]: 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,W):[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,V,W):[189]: 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,V,W):[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,V,W):[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,V,W):[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,V,W):[193]: 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,W):[194]: 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,W):[195]: 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,W):[196]: 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,W):[197]...: 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,W):[198]...: 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,W):[199]...: 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,W):[200]...: 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,W):[201]...: 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,V,W):[202]...: 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,V,W):[203]...: 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,V,W):[204]...: 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,V,W):[205]...: 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,V,W):[206]...: 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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[211]...: 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,V,W):[212]...: 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,V,W):[213]...: 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,W):[214]...: 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,W):[215]...: 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,W):[216]...: 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,W):[217]...: 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,V,W):[218]...: 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,V,W):[219]...: 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,V,W):[220]...: 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,V,W):[221]...: 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,V,W):[222]...: 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,V,W):[223]...: 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,V,W):[224]...: 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,V,W):[225]...: 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,V,W):[226]...: 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,V,W):[227]...: 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,V,W):[228]...: 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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[233]...: 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,W):[234]...: 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,W):[235]...: 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,W):[236]...: 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,W):[237]...: 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,W):[238]...: 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,W):[239]...: 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,W):[240]...: 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,W):[241]...: 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,W):[242]...: 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,W):[243]...: 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,W):[244]...: 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,W):[245]...: 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,W):[246]...: 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,W):[247]...: 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,W):[248]...: 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,W):[249]...: 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,W):[250]...: 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,W):[251]...: 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,W):[252]...: 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,W):[253]...: 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,W):[254]...: 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,W):[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,V,W):[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,V,W):[257]...: 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,W):[258]...: 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,W):[259]...: 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,W):[260]...: 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,W):[261]...: 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,W):[262]...: 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,W):[263]...: 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,W):[264]...: 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,W):[265]...: 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,W):[266]...: 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,W):[267]...: 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,W):[268]...: 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,W):[269]...: 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,W):[270]...: 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,W):[271]...: 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,W):[272]...: 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,W):[273]...: 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,W):[274]...: 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,W):[275]...: 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,W):[276]...: 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,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[284]...: 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,W): f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[105]: 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,V,W):[106]: 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,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[111]: 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,V,W):[112]: 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,V,W):[113]: 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,V,W):[114]: 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,V,W):[115]: 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,V,W):[116]: 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,V,W):[117]: 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,V,W):[118]: 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,V,W):[119]: 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,V,W):[120]: 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,V,W):[121]: 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,W):[122]: 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,W):[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,V,W):[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,V,W):[125]: 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,V,W):[126]: 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,V,W):[127]: 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,V,W):[128]: 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,V,W):[129]: 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,V,W):[130]: 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,V,W):[131]: 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,V,W):[132]: 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,V,W):[133]: 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,V,W):[134]: 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,V,W):[135]: 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,V,W):[136]: 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,V,W):[137]: 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,W):[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,W):[139]: 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,W):[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,W):[141]: 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,V,W):[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,W):[143]: 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,V,W):[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,W):[145]: 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,V,W):[146]: 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,W):[147]: 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,V,W):[148]: 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,W):[149]: 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,W):[150]: 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,W):[151]: 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,W):[152]: 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,W):[153]: 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,V,W):[154]: 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,W):[155]: 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,V,W):[156]: 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,W):[157]: -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,W):[158]: 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,W):[159]: -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,W):[160]: 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,W):[161]: -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,V,W):[162]: 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,W):[163]: -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,V,W):[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,V,W):[165]: -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,W):[166]: 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,W):[167]: -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,W):[168]: 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,W):[169]: -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,V,W):[170]: 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,W):[171]: -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,V,W):[172]: 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,W):[173]: -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,W):[174]: 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,W):[175]: -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,W):[176]: 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,W):[177]: -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,V,W):[178]: 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,W):[179]: -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,V,W):[180]: 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,W):[181]: -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,V,W):[182]: 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,W):[183]: -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,V,W):[184]: 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,W):[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,V,W):[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,V,W):[187]: -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,W):[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,V,W):[189]: -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,V,W):[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,V,W):[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,V,W):[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,V,W):[193]: 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,W):[194]: 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,W):[195]: -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,W):[196]: -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,W):[197]...: 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,W):[198]...: 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,W):[199]...: 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,W):[200]...: 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,W):[201]...: 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,V,W):[202]...: 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,V,W):[203]...: 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,V,W):[204]...: 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,V,W):[205]...: 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,V,W):[206]...: 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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[211]...: 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,V,W):[212]...: 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,V,W):[213]...: 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,W):[214]...: 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,W):[215]...: 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,W):[216]...: 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,W):[217]...: 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,V,W):[218]...: 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,V,W):[219]...: 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,V,W):[220]...: 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,V,W):[221]...: 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,V,W):[222]...: 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,V,W):[223]...: 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,V,W):[224]...: 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,V,W):[225]...: 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,V,W):[226]...: 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,V,W):[227]...: 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,V,W):[228]...: 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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[233]...: 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,W):[234]...: 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,W):[235]...: 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,W):[236]...: 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,W):[237]...: 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,W):[238]...: 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,W):[239]...: 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,W):[240]...: 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,W):[241]...: 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,W):[242]...: 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,W):[243]...: 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,W):[244]...: 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,W):[245]...: 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,W):[246]...: 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,W):[247]...: 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,W):[248]...: 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,W):[249]...: 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,W):[250]...: 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,W):[251]...: 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,W):[252]...: 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,W):[253]...: 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,W):[254]...: 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,W):[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,V,W):[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,V,W):[257]...: 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,W):[258]...: 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,W):[259]...: 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,W):[260]...: 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,W):[261]...: 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,W):[262]...: 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,W):[263]...: 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,W):[264]...: 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,W):[265]...: 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,W):[266]...: 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,W):[267]...: 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,W):[268]...: 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,W):[269]...: 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,W):[270]...: 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,W):[271]...: 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,W):[272]...: 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,W):[273]...: 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,W):[274]...: 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,W):[275]...: 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,W):[276]...: 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,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[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,V,W):[284]...: 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,W): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 69 ms. Invariants computed in 317 ms. ----Backward Invariants 202 ms. ----Transitive Invariants 30 ms. Refinement performed in 918 ms. Termination proved in 80 ms. Upper bounds computed in 742 ms. ----Phase cost structures 532 ms. --------Equation cost structures 515 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 142 ms. ----Solving cost expressions 9 ms. Compressed phase information: 12 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 2267 ms.