warning: Ignored call to loop_cont_eval2/4 in equation eval1/4 
warning: Ignored call to loop_cont_eval2/4 in equation eval1/4 
Inferred cost of eval3(A,B,C,D,E,F,G,H,I): 
eval3(A,B,C,D,E,F,G,H,I):[22]: 1
  with precondition: [E=0,D=2*A,D=2*C,D=2*F,D=2*H,B=G,D=I,B>=2,B>=D+1] 

eval3(A,B,C,D,E,F,G,H,I):[23]: 0
  with precondition: [E=1,D=2*A,D=2*C,D=2*F,D=2*H,B=G,D=I,B>=2] 

eval3(A,B,C,D,E,F,G,H,I):[24]: 1
  with precondition: [E=0,D=2*A,D=2*C,D=2*F,D=2*H,B=G,D+1=I,B>=2,B>=D+1] 

eval3(A,B,C,D,E,F,G,H,I):[25]: 1
  with precondition: [E=0,B=2*A,B=2*C,B=2*F,B=2*H,B=D,B=G,B=I,B>=2] 

eval3(A,B,C,D,E,F,G,H,I):[[19,20],21,23]: 1+it1*(1)+it2*(1)
  Such that:it1=<-2*A+1*H,it1=<-2*F+1*H,it1=<1*G+ -1,it1=<1*H+ -1,it1=<1*H+ -2*C,it1=<1*H+ -1*D,it1=<1/2*I+ -1,it1+it2=<-2*A+1*H,it1+it2=<-2*F+1*H,it1+it2=<1*G+ -1,it1+it2=<1*H+ -1,it1+it2=<1*H+ -2*C,it1+it2=<1*H+ -1*D,it1+it2=<1/2*I+ -1,it2=<-2/3*A+1/3*H,it2=<-2/3*F+1/3*H,it2=<1/3*G+ -1/3,it2=<1/3*H+ -2/3*C,it2=<1/3*H+ -1/3*D,it2=<1/3*H+ -1/3,it2=<1/6*I+ -1/3
  with precondition: [E=1,I=2*B,D=2*C,I=2*G,I=2*H,A=F,D>=1,I>=4*D,D>=2*A] 

eval3(A,B,C,D,E,F,G,H,I):[[19,20],22]: 1+it1*(1)+it2*(1)
  Such that:it1=<-2*A+1*G,it1=<-2*A+1*I,it1=<-2*F+1*G,it1=<-2*F+2*H,it1=<1*B+ -2,it1=<1*B+ -1,it1=<1*G+ -1,it1=<1*G+ -2*C,it1=<1*G+ -1*D,it1=<1*I+ -1,it1=<1*I+ -2*C,it1=<1*I+ -1*D,it1=<2*H+ -1,it1+it2=<-2*A+1*G,it1+it2=<-2*A+1*I,it1+it2=<-2*F+1*G,it1+it2=<-2*F+2*H,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<1*G+ -1,it1+it2=<1*G+ -2*C,it1+it2=<1*G+ -1*D,it1+it2=<1*I+ -1,it1+it2=<1*I+ -2*C,it1+it2=<1*I+ -1*D,it1+it2=<2*H+ -1,it2=<-2/3*A+1/3*G,it2=<-2/3*A+1/3*I,it2=<-2/3*F+1/3*G,it2=<-2/3*F+2/3*H,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<1/3*G+ -2/3*C,it2=<1/3*G+ -1/3*D,it2=<1/3*G+ -1/3,it2=<1/3*I+ -2/3*C,it2=<1/3*I+ -1/3*D,it2=<1/3*I+ -1/3,it2=<2/3*H+ -1/3
  with precondition: [E=0,D=2*C,I=2*H,A=F,B=G,D>=1,D>=2*A,I>=2*D,B>=I+1] 

eval3(A,B,C,D,E,F,G,H,I):[[19,20],23]: 0+it1*(1)+it2*(1)
  Such that:it1=<-2*A+1*G,it1=<-2*A+1*I,it1=<-2*F+1*B,it1=<-2*F+1*G,it1=<-2*F+2*H,it1=<1*B+ -1,it1=<1*G+ -1,it1=<1*G+ -2*C,it1=<1*G+ -1*D,it1=<1*I+ -1,it1=<1*I+ -2*C,it1=<1*I+ -1*D,it1=<2*B+ -1,it1=<2*H+ -1,it1+it2=<-2*A+1*G,it1+it2=<-2*A+1*I,it1+it2=<-2*F+1*B,it1+it2=<-2*F+1*G,it1+it2=<-2*F+2*H,it1+it2=<1*B+ -1,it1+it2=<1*G+ -1,it1+it2=<1*G+ -2*C,it1+it2=<1*G+ -1*D,it1+it2=<1*I+ -1,it1+it2=<1*I+ -2*C,it1+it2=<1*I+ -1*D,it1+it2=<2*B+ -1,it1+it2=<2*H+ -1,it2=<-2/3*A+1/3*G,it2=<-2/3*A+1/3*I,it2=<-2/3*F+1/3*B,it2=<-2/3*F+1/3*G,it2=<-2/3*F+1/3*I,it2=<1/3*B+ -1/3,it2=<1/3*G+ -2/3*C,it2=<1/3*G+ -1/3*D,it2=<1/3*G+ -1/3,it2=<1/3*I+ -2/3*C,it2=<1/3*I+ -1/3*D,it2=<1/3*I+ -1/3,it2=<2/3*B+ -1/3,it2=<2/3*H+ -1/3
  with precondition: [E=1,D=2*C,I=2*H,A=F,B=G,D>=1,D>=2*A,I>=2*D,B>=D+1,2*B>=I] 

eval3(A,B,C,D,E,F,G,H,I):[[19,20],24]: 1+it1*(1)+it2*(1)
  Such that:it1=<-2*A+1*G,it1=<-2*F+1*G,it1=<-2*F+2*H,it1=<1*B+ -2,it1=<1*B+ -1,it1=<1*G+ -1,it1=<1*G+ -2*C,it1=<1*G+ -1*D,it1=<1*I+ -2,it1=<2*H+ -1,it1=<-2*A+1*I+ -1,it1=<1*I+ -2*C+ -1,it1=<1*I+ -1*D+ -1,it1+it2=<-2*A+1*G,it1+it2=<-2*F+1*G,it1+it2=<-2*F+2*H,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<1*G+ -1,it1+it2=<1*G+ -2*C,it1+it2=<1*G+ -1*D,it1+it2=<1*I+ -2,it1+it2=<2*H+ -1,it1+it2=<-2*A+1*I+ -1,it1+it2=<1*I+ -2*C+ -1,it1+it2=<1*I+ -1*D+ -1,it2=<-2/3*A+1/3*G,it2=<-2/3*F+1/3*G,it2=<-2/3*F+2/3*H,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<1/3*G+ -2/3*C,it2=<1/3*G+ -1/3*D,it2=<1/3*G+ -1/3,it2=<1/3*I+ -2/3,it2=<2/3*H+ -1/3,it2=<-2/3*A+1/3*I+ -1/3,it2=<1/3*I+ -2/3*C+ -1/3,it2=<1/3*I+ -1/3*D+ -1/3
  with precondition: [E=0,D=2*C,I=2*H+1,A=F,B=G,D>=1,D>=2*A,I>=2*D+1,B>=I] 

eval3(A,B,C,D,E,F,G,H,I):[[19,20],25]: 1+it1*(1)+it2*(1)
  Such that:it1=<-2*A+2*H,it1=<-2*F+2*H,it1=<1*G+ -1,it1=<1*I+ -1,it1=<2*H+ -1,it1=<2*H+ -2*C,it1=<2*H+ -1*D,it1+it2=<-2*A+2*H,it1+it2=<-2*F+2*H,it1+it2=<1*G+ -1,it1+it2=<1*I+ -1,it1+it2=<2*H+ -1,it1+it2=<2*H+ -2*C,it1+it2=<2*H+ -1*D,it2=<-2/3*A+2/3*H,it2=<-2/3*F+2/3*H,it2=<1/3*G+ -1/3,it2=<1/3*I+ -1/3,it2=<2/3*H+ -2/3*C,it2=<2/3*H+ -1/3*D,it2=<2/3*H+ -1/3
  with precondition: [E=0,D=2*C,I=2*H,I=B,A=F,I=G,D>=1,D>=2*A,I>=2*D] 

eval3(A,B,C,D,E,F,G,H,I):[21,23]: 1
  with precondition: [E=1,B=2*A,B=2*C,B=2*F,B=D,B=G,B=H,2*B=I,B>=2] 

Inferred cost of eval2(A,B,C,D,E,F,G,H,I): 
eval2(A,B,C,D,E,F,G,H,I):[39]: 1
  with precondition: [E=1,B>=2] 

eval2(A,B,C,D,E,F,G,H,I):[40]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*B+ -1,it1=<1*B+ -2*A,it1+it2=<1*B+ -1,it1+it2=<1*B+ -2*A,it2=<1/3*B+ -2/3*A,it2=<1/3*B+ -1/3
  with precondition: [E=1,2*A>=1,B>=4*A] 

eval2(A,B,C,D,E,F,G,H,I):[41]: 1+it1*(1)+it2*(1)
  Such that:it1=<-2*A+2*B,it1=<1*B+ -1,it1=<1*B+ -2*A,it1=<2*B+ -1,it1+it2=<-2*A+2*B,it1+it2=<1*B+ -1,it1+it2=<1*B+ -2*A,it1+it2=<2*B+ -1,it2=<-2/3*A+2/3*B,it2=<1/3*B+ -2/3*A,it2=<1/3*B+ -1/3,it2=<2/3*B+ -1/3
  with precondition: [E=1,2*A>=1,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[42]: 2
  with precondition: [E=1,2*A=B,A>=1] 

eval2(A,B,C,D,E,F,G,H,I):[43]: 0
  with precondition: [E=1,F=A,G=B,H=C,I=D] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],[33,34,36,37,38],35,43]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -1,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,F=1,G=1,H=1,I=2,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],[33,34,36,37,38],39]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -1,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],[33,34,36,37,38],40]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it2+it3+it4+it7=<1*B+ -3,it2+it3+it4+it7=<1*B+ -10/3,it2+it4=<1*B+ -3,it2+it4=<1*B+ -10/3,it2+it7=<1*B+ -3,it2+it7=<1*B+ -10/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3,it10+it11+it14=<1*A+ -1,it10+it11+it14=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],[33,34,36,37,38],41]: 1+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*B+ -3,it1+it2+it3+it4+it7=<2*B+ -2,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*B+ -3,it1+it2+it4=<2*B+ -2,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*B+ -3,it1+it2+it7=<2*B+ -2,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*B+ -3,it1+it3+it4+it7=<2*B+ -2,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*B+ -3,it1+it4=<2*B+ -2,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*B+ -3,it1+it7=<2*B+ -2,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it3+it4+it7=<1*B+ -5/3,it2+it3+it4+it7=<1*B+ -4/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it4=<1*B+ -5/3,it2+it4=<1*B+ -4/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it2+it7=<1*B+ -5/3,it2+it7=<1*B+ -4/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3,it10+it11+it14=<1*A+ -1,it10+it11+it14=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],[33,34,36,37,38],42]: 2+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -1,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],[33,34,36,37,38],43]: 0+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<1*B+ -1*G,it2=<1*B+ -4,it2=<1*B+ -1*G,it5=<1*B+ -3,it5=<1*B+ -1*G,it8+it9+it12=<1*A+ -1,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,F=1,A>=2,H>=1,B>=2*A+1,I>=2*H,B>=G+1,G>=H+1,G+1>=I,2*H+1>=I] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],39]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -1,it1+it2+it5=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],40]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it3+it4+it7=<1*A+ -1,it3+it4+it7=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],41]: 1+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*B+ -2,it1=<2*B+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*B+ -2,it1+it2=<2*B+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*B+ -2/3,it2=<2/3*B+ -1/3,it3+it4+it7=<1*A+ -1,it3+it4+it7=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [E=1,A>=2,B>=2*A+1] 

eval2(A,B,C,D,E,F,G,H,I):[[27,28,30,31,32],43]: 0+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -1,it1+it2+it5=<1*A+ -1*F,it1+it2+it5=<1/2*B+ -3/2,it1+it2+it5=<1/2*G+ -3/2,it1+it2+it5=<-1*F+1/2*B+ -1/2,it1+it2+it5=<-1*F+1/2*G+ -1/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [E=1,B=G,F>=1,B>=2*A+1,I>=2*H,A>=F+1,H>=F+1,B>=I,2*H+1>=I,2*B>=3*H+F+3] 

eval2(A,B,C,D,E,F,G,H,I):[[33,34,36,37,38],35,43]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=1,E=1,F=1,G=1,H=1,I=2,B>=3] 

eval2(A,B,C,D,E,F,G,H,I):[[33,34,36,37,38],39]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=1,E=1,B>=3] 

eval2(A,B,C,D,E,F,G,H,I):[[33,34,36,37,38],40]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it2+it3+it4+it7=<1*B+ -3,it2+it3+it4+it7=<1*B+ -10/3,it2+it4=<1*B+ -3,it2+it4=<1*B+ -10/3,it2+it7=<1*B+ -3,it2+it7=<1*B+ -10/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
  with precondition: [A=1,E=1,B>=5] 

eval2(A,B,C,D,E,F,G,H,I):[[33,34,36,37,38],41]: 1+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*B+ -3,it1+it2+it3+it4+it7=<2*B+ -2,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*B+ -3,it1+it2+it4=<2*B+ -2,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*B+ -3,it1+it2+it7=<2*B+ -2,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*B+ -3,it1+it3+it4+it7=<2*B+ -2,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*B+ -3,it1+it4=<2*B+ -2,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*B+ -3,it1+it7=<2*B+ -2,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it3+it4+it7=<1*B+ -5/3,it2+it3+it4+it7=<1*B+ -4/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it4=<1*B+ -5/3,it2+it4=<1*B+ -4/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it2+it7=<1*B+ -5/3,it2+it7=<1*B+ -4/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
  with precondition: [A=1,E=1,B>=4] 

eval2(A,B,C,D,E,F,G,H,I):[[33,34,36,37,38],42]: 2+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=1,E=1,B>=3] 

eval2(A,B,C,D,E,F,G,H,I):[[33,34,36,37,38],43]: 0+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<1*B+ -1*G,it2=<1*B+ -4,it2=<1*B+ -1*G,it5=<1*B+ -3,it5=<1*B+ -1*G
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=1,E=1,F=1,H>=1,I>=2*H,B>=G+1,G>=H+1,G+1>=I,2*H+1>=I] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],[33,34,36,37,38],35,43]: 6+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -4,it2=<2*A+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -3,it5=<2*A+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -1/3,it11=<2/3*A+ -2/3,it11=<2/3*A+ -4/3,it11=<2/3*A+ -5/3,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -1,it10+it11=<2*A+ -2,it10+it11=<2*A+ -4,it10+it11=<2*A+ -5,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -1,it10=<2*A+ -2,it10=<2*A+ -4,it10=<2*A+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1/3,it14=<2/3*A+ -4/3,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -1,it13+it14=<2*A+ -4,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -1,it13=<2*A+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,F=1,G=1,H=1,I=2,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],[33,34,36,37,38],39]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -4,it2=<2*A+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -3,it5=<2*A+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -1/3,it11=<2/3*A+ -2/3,it11=<2/3*A+ -4/3,it11=<2/3*A+ -5/3,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -1,it10+it11=<2*A+ -2,it10+it11=<2*A+ -4,it10+it11=<2*A+ -5,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -1,it10=<2*A+ -2,it10=<2*A+ -4,it10=<2*A+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1/3,it14=<2/3*A+ -4/3,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -1,it13+it14=<2*A+ -4,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -1,it13=<2*A+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],[33,34,36,37,38],40]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*A+ -2,it1+it2+it3+it4+it7=<2*A+ -1,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*A+ -2,it1+it2+it4=<2*A+ -1,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*A+ -2,it1+it2+it7=<2*A+ -1,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*A+ -2,it1+it3+it4+it7=<2*A+ -1,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*A+ -2,it1+it4=<2*A+ -1,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*A+ -2,it1+it7=<2*A+ -1,it2+it3+it4+it7=<1*B+ -3,it2+it3+it4+it7=<1*B+ -10/3,it2+it3+it4+it7=<2*A+ -3,it2+it3+it4+it7=<2*A+ -10/3,it2+it4=<1*B+ -3,it2+it4=<1*B+ -10/3,it2+it4=<2*A+ -3,it2+it4=<2*A+ -10/3,it2+it7=<1*B+ -3,it2+it7=<1*B+ -10/3,it2+it7=<2*A+ -3,it2+it7=<2*A+ -10/3,it3+it4+it7=<1*B+ -2,it3+it4+it7=<2*A+ -2,it4=<1*B+ -4,it4=<2*A+ -4,it7=<1*B+ -3,it7=<2*A+ -3,it10+it11+it14=<1*A+ -2,it10+it11+it14=<1/2*B+ -2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<2/3*A+ -1/3,it13=<2/3*A+ -2/3,it13=<2/3*A+ -4/3,it13=<2/3*A+ -5/3,it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<2*A+ -1,it12+it13=<2*A+ -2,it12+it13=<2*A+ -4,it12+it13=<2*A+ -5,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<2*A+ -1,it12=<2*A+ -2,it12=<2*A+ -4,it12=<2*A+ -5,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<2/3*A+ -1/3,it16=<2/3*A+ -4/3,it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<2*A+ -1,it15+it16=<2*A+ -4,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<2*A+ -1,it15=<2*A+ -4,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],[33,34,36,37,38],41]: 4+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*A+ -2,it1+it2+it3+it4+it7=<2*A+ -1,it1+it2+it3+it4+it7=<2*B+ -3,it1+it2+it3+it4+it7=<2*B+ -2,it1+it2+it3+it4+it7=<4*A+ -3,it1+it2+it3+it4+it7=<4*A+ -2,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*A+ -2,it1+it2+it4=<2*A+ -1,it1+it2+it4=<2*B+ -3,it1+it2+it4=<2*B+ -2,it1+it2+it4=<4*A+ -3,it1+it2+it4=<4*A+ -2,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*A+ -2,it1+it2+it7=<2*A+ -1,it1+it2+it7=<2*B+ -3,it1+it2+it7=<2*B+ -2,it1+it2+it7=<4*A+ -3,it1+it2+it7=<4*A+ -2,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*A+ -2,it1+it3+it4+it7=<2*A+ -1,it1+it3+it4+it7=<2*B+ -3,it1+it3+it4+it7=<2*B+ -2,it1+it3+it4+it7=<4*A+ -3,it1+it3+it4+it7=<4*A+ -2,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*A+ -2,it1+it4=<2*A+ -1,it1+it4=<2*B+ -3,it1+it4=<2*B+ -2,it1+it4=<4*A+ -3,it1+it4=<4*A+ -2,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*A+ -2,it1+it7=<2*A+ -1,it1+it7=<2*B+ -3,it1+it7=<2*B+ -2,it1+it7=<4*A+ -3,it1+it7=<4*A+ -2,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it3+it4+it7=<1*B+ -5/3,it2+it3+it4+it7=<1*B+ -4/3,it2+it3+it4+it7=<2*A+ -8/3,it2+it3+it4+it7=<2*A+ -7/3,it2+it3+it4+it7=<2*A+ -5/3,it2+it3+it4+it7=<2*A+ -4/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it4=<1*B+ -5/3,it2+it4=<1*B+ -4/3,it2+it4=<2*A+ -8/3,it2+it4=<2*A+ -7/3,it2+it4=<2*A+ -5/3,it2+it4=<2*A+ -4/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it2+it7=<1*B+ -5/3,it2+it7=<1*B+ -4/3,it2+it7=<2*A+ -8/3,it2+it7=<2*A+ -7/3,it2+it7=<2*A+ -5/3,it2+it7=<2*A+ -4/3,it3+it4+it7=<1*B+ -2,it3+it4+it7=<2*A+ -2,it4=<1*B+ -4,it4=<2*A+ -4,it7=<1*B+ -3,it7=<2*A+ -3,it10+it11+it14=<1*A+ -2,it10+it11+it14=<1/2*B+ -2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<2/3*A+ -1/3,it13=<2/3*A+ -2/3,it13=<2/3*A+ -4/3,it13=<2/3*A+ -5/3,it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<2*A+ -1,it12+it13=<2*A+ -2,it12+it13=<2*A+ -4,it12+it13=<2*A+ -5,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<2*A+ -1,it12=<2*A+ -2,it12=<2*A+ -4,it12=<2*A+ -5,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<2/3*A+ -1/3,it16=<2/3*A+ -4/3,it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<2*A+ -1,it15+it16=<2*A+ -4,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<2*A+ -1,it15=<2*A+ -4,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],[33,34,36,37,38],42]: 5+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -4,it2=<2*A+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -3,it5=<2*A+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -1/3,it11=<2/3*A+ -2/3,it11=<2/3*A+ -4/3,it11=<2/3*A+ -5/3,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -1,it10+it11=<2*A+ -2,it10+it11=<2*A+ -4,it10+it11=<2*A+ -5,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -1,it10=<2*A+ -2,it10=<2*A+ -4,it10=<2*A+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1/3,it14=<2/3*A+ -4/3,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -1,it13+it14=<2*A+ -4,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -1,it13=<2*A+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],[33,34,36,37,38],43]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<1*B+ -1*G,it1+it2+it5=<2*A+ -2,it1+it2+it5=<2*A+ -1*G,it2=<1*B+ -4,it2=<1*B+ -1*G,it2=<2*A+ -4,it2=<2*A+ -1*G,it5=<1*B+ -3,it5=<1*B+ -1*G,it5=<2*A+ -3,it5=<2*A+ -1*G,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -1/3,it11=<2/3*A+ -2/3,it11=<2/3*A+ -4/3,it11=<2/3*A+ -5/3,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -1,it10+it11=<2*A+ -2,it10+it11=<2*A+ -4,it10+it11=<2*A+ -5,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -1,it10=<2*A+ -2,it10=<2*A+ -4,it10=<2*A+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1/3,it14=<2/3*A+ -4/3,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -1,it13+it14=<2*A+ -4,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -1,it13=<2*A+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [E=1,F=1,2*A=B,A>=3,H>=1,I>=2*H,2*A>=G+1,G>=H+1,G+1>=I,2*H+1>=I] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],39]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -2,it1+it2+it5=<1/2*B+ -2
            it4=<2/3*A+ -1/3,it4=<2/3*A+ -2/3,it4=<2/3*A+ -4/3,it4=<2/3*A+ -5/3,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<2*A+ -1,it3+it4=<2*A+ -2,it3+it4=<2*A+ -4,it3+it4=<2*A+ -5,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<2*A+ -1,it3=<2*A+ -2,it3=<2*A+ -4,it3=<2*A+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<2/3*A+ -1/3,it7=<2/3*A+ -4/3,it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<2*A+ -1,it6+it7=<2*A+ -4,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<2*A+ -1,it6=<2*A+ -4,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],40]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*A+ -2,it1=<2*A+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*A+ -2,it1+it2=<2*A+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*A+ -2/3,it2=<2/3*A+ -1/3,it3+it4+it7=<1*A+ -2,it3+it4+it7=<1/2*B+ -2
            it6=<2/3*A+ -1/3,it6=<2/3*A+ -2/3,it6=<2/3*A+ -4/3,it6=<2/3*A+ -5/3,it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<2*A+ -1,it5+it6=<2*A+ -2,it5+it6=<2*A+ -4,it5+it6=<2*A+ -5,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<2*A+ -1,it5=<2*A+ -2,it5=<2*A+ -4,it5=<2*A+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<2/3*A+ -1/3,it9=<2/3*A+ -4/3,it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<2*A+ -1,it8+it9=<2*A+ -4,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<2*A+ -1,it8=<2*A+ -4,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],41]: 4+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*A+ -2,it1=<2*A+ -1,it1=<2*B+ -2,it1=<2*B+ -1,it1=<4*A+ -2,it1=<4*A+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*A+ -2,it1+it2=<2*A+ -1,it1+it2=<2*B+ -2,it1+it2=<2*B+ -1,it1+it2=<4*A+ -2,it1+it2=<4*A+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*A+ -2/3,it2=<2/3*A+ -1/3,it2=<2/3*B+ -2/3,it2=<2/3*B+ -1/3,it2=<4/3*A+ -2/3,it2=<4/3*A+ -1/3,it3+it4+it7=<1*A+ -2,it3+it4+it7=<1/2*B+ -2
            it6=<2/3*A+ -1/3,it6=<2/3*A+ -2/3,it6=<2/3*A+ -4/3,it6=<2/3*A+ -5/3,it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<2*A+ -1,it5+it6=<2*A+ -2,it5+it6=<2*A+ -4,it5+it6=<2*A+ -5,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<2*A+ -1,it5=<2*A+ -2,it5=<2*A+ -4,it5=<2*A+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<2/3*A+ -1/3,it9=<2/3*A+ -4/3,it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<2*A+ -1,it8+it9=<2*A+ -4,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<2*A+ -1,it8=<2*A+ -4,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [E=1,2*A=B,A>=3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[27,28,30,31,32],43]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -2,it1+it2+it5=<1/2*B+ -2,it1+it2+it5=<1/2*G+ -2,it1+it2+it5=<1*A+ -1*F+ -1,it1+it2+it5=<1/2*B+ -1*F+ -1,it1+it2+it5=<1/2*G+ -1*F+ -1
            it4=<2/3*A+ -1/3,it4=<2/3*A+ -2/3,it4=<2/3*A+ -4/3,it4=<2/3*A+ -5/3,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<2*A+ -1,it3+it4=<2*A+ -2,it3+it4=<2*A+ -4,it3+it4=<2*A+ -5,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<2*A+ -1,it3=<2*A+ -2,it3=<2*A+ -4,it3=<2*A+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<2/3*A+ -1/3,it7=<2/3*A+ -4/3,it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<2*A+ -1,it6+it7=<2*A+ -4,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<2*A+ -1,it6=<2*A+ -4,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [E=1,B=2*A,B=G,F>=1,I>=2*H,H>=F+1,B>=I,2*H+1>=I,B>=F+H+3,H+2*B>=2*I+F+3] 

eval2(A,B,C,D,E,F,G,H,I):[29,[33,34,36,37,38],35,43]: 6+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it2=<1,it2=<2
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=2,B=4,E=1,F=1,G=1,H=1,I=2] 

eval2(A,B,C,D,E,F,G,H,I):[29,[33,34,36,37,38],39]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it2=<1,it2=<2
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=2,B=4,E=1] 

eval2(A,B,C,D,E,F,G,H,I):[29,[33,34,36,37,38],41]: 4+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))
  Such that:it1=<1,it1=<2,it1=<3,it1=<4,it1=<5,it1=<6,it1=<7,it1=<9,it1+it2=<1,it1+it2=<2,it1+it2=<3,it1+it2=<4,it1+it2=<5,it1+it2=<6,it1+it2=<7,it1+it2=<9,it2=<1,it2=<2,it2=<3,it2=<1/3,it2=<2/3,it2=<4/3,it2=<5/3,it2=<7/3,it3+it4=<1,it3+it4=<2,it4=<1
            it6=<2/3,it6=<1,it5+it6=<3,it5+it6=<2,it5=<3,it5=<2
  with precondition: [A=2,B=4,E=1] 

eval2(A,B,C,D,E,F,G,H,I):[29,[33,34,36,37,38],42]: 5+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it2=<1,it2=<2
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=2,B=4,E=1] 

eval2(A,B,C,D,E,F,G,H,I):[29,[33,34,36,37,38],43]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it1+it2=<3,it1+it2=<-2*H+5,it1+it2=<-1*G+4,it1+it2=<-1*H+3,it1+it2=<-1*I+5,it2=<1,it2=<2,it2=<3,it2=<-2*H+5,it2=<-1*G+4,it2=<-1*H+3,it2=<-1*I+5
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=2,B=4,E=1,F=1,3>=G,H>=1,I>=2*H,G>=H+1,H+2>=I] 

eval2(A,B,C,D,E,F,G,H,I):[29,39]: 4
  with precondition: [E=1,2*A=B,A>=2] 

eval2(A,B,C,D,E,F,G,H,I):[29,40]: 5+it1*(1)+it2*(1)
  Such that:it1=<2,it1=<3,it1+it2=<2,it1+it2=<3,it2=<1,it2=<2/3
  with precondition: [A=2,B=4,E=1] 

eval2(A,B,C,D,E,F,G,H,I):[29,41]: 4+it1*(1)+it2*(1)
  Such that:it1=<2,it1=<1*B+ -1,it1=<1*B+2,it1=<2*A+ -1,it1=<2*A+2,it1=<2*B+ -1,it1=<4*A+ -1,it1+it2=<2,it1+it2=<1*B+ -1,it1+it2=<1*B+2,it1+it2=<2*A+ -1,it1+it2=<2*A+2,it1+it2=<2*B+ -1,it1+it2=<4*A+ -1,it2=<1/3*B+ -1/3,it2=<1/3*B+2/3,it2=<2/3*A+ -1/3,it2=<2/3*A+2/3,it2=<2/3*B+ -1/3,it2=<4/3*A+ -1/3,it2=<2/3
  with precondition: [E=1,2*A=B,A>=2] 

eval2(A,B,C,D,E,F,G,H,I):[29,43]: 3
  with precondition: [E=1,B=2*A,B=2*F+2,B=2*H,B=G,B=I,B>=4] 

eval2(A,B,C,D,E,F,G,H,I):[35,43]: 3
  with precondition: [A=1,B=2,E=1,F=1,G=1,H=1,I=2] 

Inferred cost of eval1(A,B,C,D): 
eval1(A,B,C,D):[45]: 2
  with precondition: [A>=2,B>=2] 

eval1(A,B,C,D):[46]: 3+it1*(1)+it2*(1)
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<1*B+ -2*A+2,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<1*B+ -2*A+2,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<1/3*B+ -2/3*A+2/3
  with precondition: [A>=2,B+4>=4*A] 

eval1(A,B,C,D):[47]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*B+ -2,it1=<2*B+ -1,it1=<1*B+ -2*A+2,it1=<2*B+ -2*A+2,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*B+ -2,it1+it2=<2*B+ -1,it1+it2=<1*B+ -2*A+2,it1+it2=<2*B+ -2*A+2,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*B+ -2/3,it2=<2/3*B+ -1/3,it2=<1/3*B+ -2/3*A+2/3,it2=<2/3*B+ -2/3*A+2/3
  with precondition: [A>=2,B+1>=2*A] 

eval1(A,B,C,D):[48]: 3
  with precondition: [2*A=B+2,A>=2] 

eval1(A,B,C,D):[49]: 1
  with precondition: [A>=2] 

eval1(A,B,C,D):[50]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[51]: 2+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[52]: 3+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it2+it3+it4+it7=<1*B+ -3,it2+it3+it4+it7=<1*B+ -10/3,it2+it4=<1*B+ -3,it2+it4=<1*B+ -10/3,it2+it7=<1*B+ -3,it2+it7=<1*B+ -10/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3,it10+it11+it14=<1*A+ -2,it10+it11+it14=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[53]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*B+ -3,it1+it2+it3+it4+it7=<2*B+ -2,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*B+ -3,it1+it2+it4=<2*B+ -2,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*B+ -3,it1+it2+it7=<2*B+ -2,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*B+ -3,it1+it3+it4+it7=<2*B+ -2,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*B+ -3,it1+it4=<2*B+ -2,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*B+ -3,it1+it7=<2*B+ -2,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it3+it4+it7=<1*B+ -5/3,it2+it3+it4+it7=<1*B+ -4/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it4=<1*B+ -5/3,it2+it4=<1*B+ -4/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it2+it7=<1*B+ -5/3,it2+it7=<1*B+ -4/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3,it10+it11+it14=<1*A+ -2,it10+it11+it14=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[54]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[55]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2,it8+it9+it12=<1*A+ -2,it8+it9+it12=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[56]: 2+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -2,it1+it2+it5=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[57]: 3+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it3+it4+it7=<1*A+ -2,it3+it4+it7=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[58]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*B+ -2,it1=<2*B+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*B+ -2,it1+it2=<2*B+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*B+ -2/3,it2=<2/3*B+ -1/3,it3+it4+it7=<1*A+ -2,it3+it4+it7=<1/2*B+ -3/2
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[59]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -2,it1+it2+it5=<1/2*B+ -3/2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [A>=3,B+1>=2*A] 

eval1(A,B,C,D):[60]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=2,B>=3] 

eval1(A,B,C,D):[61]: 2+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=2,B>=3] 

eval1(A,B,C,D):[62]: 3+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it2+it3+it4+it7=<1*B+ -3,it2+it3+it4+it7=<1*B+ -10/3,it2+it4=<1*B+ -3,it2+it4=<1*B+ -10/3,it2+it7=<1*B+ -3,it2+it7=<1*B+ -10/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
  with precondition: [A=2,B>=5] 

eval1(A,B,C,D):[63]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*B+ -3,it1+it2+it3+it4+it7=<2*B+ -2,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*B+ -3,it1+it2+it4=<2*B+ -2,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*B+ -3,it1+it2+it7=<2*B+ -2,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*B+ -3,it1+it3+it4+it7=<2*B+ -2,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*B+ -3,it1+it4=<2*B+ -2,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*B+ -3,it1+it7=<2*B+ -2,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it3+it4+it7=<1*B+ -5/3,it2+it3+it4+it7=<1*B+ -4/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it4=<1*B+ -5/3,it2+it4=<1*B+ -4/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it2+it7=<1*B+ -5/3,it2+it7=<1*B+ -4/3,it3+it4+it7=<1*B+ -2,it4=<1*B+ -4,it7=<1*B+ -3
            it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<1*B+ -1,it8=<1*B+ -2
  with precondition: [A=2,B>=4] 

eval1(A,B,C,D):[64]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=2,B>=3] 

eval1(A,B,C,D):[65]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -2,it2=<1*B+ -4,it2=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -2
            it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<1*B+ -1,it6=<1*B+ -2
  with precondition: [A=2,B>=3] 

eval1(A,B,C,D):[66]: 7+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -4,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -6,it2=<2*A+ -4,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -5,it5=<2*A+ -4,it8+it9+it12=<1*A+ -3,it8+it9+it12=<1/2*B+ -2
            it4=<2/3*A+ -4/3,it4=<2/3*A+ -5/3,it4=<2/3*A+ -1,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<2*A+ -3,it3+it4=<2*A+ -4,it3+it4=<2*A+ -5,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<2*A+ -3,it3=<2*A+ -4,it3=<2*A+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<2/3*A+ -4/3,it7=<2/3*A+ -1,it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<2*A+ -3,it6+it7=<2*A+ -4,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<2*A+ -3,it6=<2*A+ -4,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -4/3,it11=<2/3*A+ -7/3,it11=<2/3*A+ -1,it11=<2/3*A+ -2,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -3,it10+it11=<2*A+ -4,it10+it11=<2*A+ -6,it10+it11=<2*A+ -7,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -3,it10=<2*A+ -4,it10=<2*A+ -6,it10=<2*A+ -7,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1,it14=<2/3*A+ -2,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -3,it13+it14=<2*A+ -6,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -3,it13=<2*A+ -6,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[67]: 5+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -4,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -6,it2=<2*A+ -4,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -5,it5=<2*A+ -4,it8+it9+it12=<1*A+ -3,it8+it9+it12=<1/2*B+ -2
            it4=<2/3*A+ -4/3,it4=<2/3*A+ -5/3,it4=<2/3*A+ -1,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<2*A+ -3,it3+it4=<2*A+ -4,it3+it4=<2*A+ -5,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<2*A+ -3,it3=<2*A+ -4,it3=<2*A+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<2/3*A+ -4/3,it7=<2/3*A+ -1,it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<2*A+ -3,it6+it7=<2*A+ -4,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<2*A+ -3,it6=<2*A+ -4,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -4/3,it11=<2/3*A+ -7/3,it11=<2/3*A+ -1,it11=<2/3*A+ -2,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -3,it10+it11=<2*A+ -4,it10+it11=<2*A+ -6,it10+it11=<2*A+ -7,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -3,it10=<2*A+ -4,it10=<2*A+ -6,it10=<2*A+ -7,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1,it14=<2/3*A+ -2,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -3,it13+it14=<2*A+ -6,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -3,it13=<2*A+ -6,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[68]: 6+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*A+ -4,it1+it2+it3+it4+it7=<2*A+ -3,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*A+ -4,it1+it2+it4=<2*A+ -3,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*A+ -4,it1+it2+it7=<2*A+ -3,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*A+ -4,it1+it3+it4+it7=<2*A+ -3,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*A+ -4,it1+it4=<2*A+ -3,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*A+ -4,it1+it7=<2*A+ -3,it2+it3+it4+it7=<1*B+ -3,it2+it3+it4+it7=<1*B+ -10/3,it2+it3+it4+it7=<2*A+ -5,it2+it3+it4+it7=<2*A+ -16/3,it2+it4=<1*B+ -3,it2+it4=<1*B+ -10/3,it2+it4=<2*A+ -5,it2+it4=<2*A+ -16/3,it2+it7=<1*B+ -3,it2+it7=<1*B+ -10/3,it2+it7=<2*A+ -5,it2+it7=<2*A+ -16/3,it3+it4+it7=<1*B+ -2,it3+it4+it7=<2*A+ -4,it4=<1*B+ -4,it4=<2*A+ -6,it7=<1*B+ -3,it7=<2*A+ -5,it10+it11+it14=<1*A+ -3,it10+it11+it14=<1/2*B+ -2
            it6=<2/3*A+ -4/3,it6=<2/3*A+ -5/3,it6=<2/3*A+ -1,it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<2*A+ -3,it5+it6=<2*A+ -4,it5+it6=<2*A+ -5,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<2*A+ -3,it5=<2*A+ -4,it5=<2*A+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<2/3*A+ -4/3,it9=<2/3*A+ -1,it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<2*A+ -3,it8+it9=<2*A+ -4,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<2*A+ -3,it8=<2*A+ -4,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<2/3*A+ -4/3,it13=<2/3*A+ -7/3,it13=<2/3*A+ -1,it13=<2/3*A+ -2,it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<2*A+ -3,it12+it13=<2*A+ -4,it12+it13=<2*A+ -6,it12+it13=<2*A+ -7,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<2*A+ -3,it12=<2*A+ -4,it12=<2*A+ -6,it12=<2*A+ -7,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<2/3*A+ -1,it16=<2/3*A+ -2,it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<2*A+ -3,it15+it16=<2*A+ -6,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<2*A+ -3,it15=<2*A+ -6,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[69]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))+it10*(3)+it11*(3+it12*(1)+it13*(1))+it14*(3+it15*(1)+it16*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<1*B+ -1,it1+it2+it3+it4+it7=<2*A+ -4,it1+it2+it3+it4+it7=<2*A+ -3,it1+it2+it3+it4+it7=<2*B+ -3,it1+it2+it3+it4+it7=<2*B+ -2,it1+it2+it3+it4+it7=<4*A+ -7,it1+it2+it3+it4+it7=<4*A+ -6,it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<2*A+ -4,it1+it2+it4=<2*A+ -3,it1+it2+it4=<2*B+ -3,it1+it2+it4=<2*B+ -2,it1+it2+it4=<4*A+ -7,it1+it2+it4=<4*A+ -6,it1+it2+it7=<1*B+ -2,it1+it2+it7=<1*B+ -1,it1+it2+it7=<2*A+ -4,it1+it2+it7=<2*A+ -3,it1+it2+it7=<2*B+ -3,it1+it2+it7=<2*B+ -2,it1+it2+it7=<4*A+ -7,it1+it2+it7=<4*A+ -6,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -1,it1+it3+it4+it7=<2*A+ -4,it1+it3+it4+it7=<2*A+ -3,it1+it3+it4+it7=<2*B+ -3,it1+it3+it4+it7=<2*B+ -2,it1+it3+it4+it7=<4*A+ -7,it1+it3+it4+it7=<4*A+ -6,it1+it4=<1*B+ -2,it1+it4=<1*B+ -1,it1+it4=<2*A+ -4,it1+it4=<2*A+ -3,it1+it4=<2*B+ -3,it1+it4=<2*B+ -2,it1+it4=<4*A+ -7,it1+it4=<4*A+ -6,it1+it7=<1*B+ -2,it1+it7=<1*B+ -1,it1+it7=<2*A+ -4,it1+it7=<2*A+ -3,it1+it7=<2*B+ -3,it1+it7=<2*B+ -2,it1+it7=<4*A+ -7,it1+it7=<4*A+ -6,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it3+it4+it7=<1*B+ -5/3,it2+it3+it4+it7=<1*B+ -4/3,it2+it3+it4+it7=<2*A+ -14/3,it2+it3+it4+it7=<2*A+ -13/3,it2+it3+it4+it7=<2*A+ -11/3,it2+it3+it4+it7=<2*A+ -10/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it4=<1*B+ -5/3,it2+it4=<1*B+ -4/3,it2+it4=<2*A+ -14/3,it2+it4=<2*A+ -13/3,it2+it4=<2*A+ -11/3,it2+it4=<2*A+ -10/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it2+it7=<1*B+ -5/3,it2+it7=<1*B+ -4/3,it2+it7=<2*A+ -14/3,it2+it7=<2*A+ -13/3,it2+it7=<2*A+ -11/3,it2+it7=<2*A+ -10/3,it3+it4+it7=<1*B+ -2,it3+it4+it7=<2*A+ -4,it4=<1*B+ -4,it4=<2*A+ -6,it7=<1*B+ -3,it7=<2*A+ -5,it10+it11+it14=<1*A+ -3,it10+it11+it14=<1/2*B+ -2
            it6=<2/3*A+ -4/3,it6=<2/3*A+ -5/3,it6=<2/3*A+ -1,it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -1,it5+it6=<2*A+ -3,it5+it6=<2*A+ -4,it5+it6=<2*A+ -5,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5=<2*A+ -3,it5=<2*A+ -4,it5=<2*A+ -5,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -3
            it9=<2/3*A+ -4/3,it9=<2/3*A+ -1,it9=<1/3*B+ -1/3,it9=<1/3*B+ -2/3,it8+it9=<2*A+ -3,it8+it9=<2*A+ -4,it8+it9=<1*B+ -1,it8+it9=<1*B+ -2,it8=<2*A+ -3,it8=<2*A+ -4,it8=<1*B+ -1,it8=<1*B+ -2
            it13=<2/3*A+ -4/3,it13=<2/3*A+ -7/3,it13=<2/3*A+ -1,it13=<2/3*A+ -2,it13=<1/3*B+ -1/3,it13=<1/3*B+ -2/3,it13=<1/3*B+ -4/3,it13=<1/3*B+ -5/3,it12+it13=<2*A+ -3,it12+it13=<2*A+ -4,it12+it13=<2*A+ -6,it12+it13=<2*A+ -7,it12+it13=<1*B+ -1,it12+it13=<1*B+ -2,it12+it13=<1*B+ -4,it12+it13=<1*B+ -5,it12=<2*A+ -3,it12=<2*A+ -4,it12=<2*A+ -6,it12=<2*A+ -7,it12=<1*B+ -1,it12=<1*B+ -2,it12=<1*B+ -4,it12=<1*B+ -5
            it16=<2/3*A+ -1,it16=<2/3*A+ -2,it16=<1/3*B+ -1/3,it16=<1/3*B+ -4/3,it15+it16=<2*A+ -3,it15+it16=<2*A+ -6,it15+it16=<1*B+ -1,it15+it16=<1*B+ -4,it15=<2*A+ -3,it15=<2*A+ -6,it15=<1*B+ -1,it15=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[70]: 6+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -4,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -6,it2=<2*A+ -4,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -5,it5=<2*A+ -4,it8+it9+it12=<1*A+ -3,it8+it9+it12=<1/2*B+ -2
            it4=<2/3*A+ -4/3,it4=<2/3*A+ -5/3,it4=<2/3*A+ -1,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<2*A+ -3,it3+it4=<2*A+ -4,it3+it4=<2*A+ -5,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<2*A+ -3,it3=<2*A+ -4,it3=<2*A+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<2/3*A+ -4/3,it7=<2/3*A+ -1,it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<2*A+ -3,it6+it7=<2*A+ -4,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<2*A+ -3,it6=<2*A+ -4,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -4/3,it11=<2/3*A+ -7/3,it11=<2/3*A+ -1,it11=<2/3*A+ -2,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -3,it10+it11=<2*A+ -4,it10+it11=<2*A+ -6,it10+it11=<2*A+ -7,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -3,it10=<2*A+ -4,it10=<2*A+ -6,it10=<2*A+ -7,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1,it14=<2/3*A+ -2,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -3,it13+it14=<2*A+ -6,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -3,it13=<2*A+ -6,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[71]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))+it8*(3)+it9*(3+it10*(1)+it11*(1))+it12*(3+it13*(1)+it14*(1))
  Such that:it1+it2+it5=<1*B+ -2,it1+it2+it5=<2*A+ -4,it2=<1*B+ -4,it2=<1*B+ -2,it2=<2*A+ -6,it2=<2*A+ -4,it5=<1*B+ -3,it5=<1*B+ -2,it5=<2*A+ -5,it5=<2*A+ -4,it8+it9+it12=<1*A+ -3,it8+it9+it12=<1/2*B+ -2
            it4=<2/3*A+ -4/3,it4=<2/3*A+ -5/3,it4=<2/3*A+ -1,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -1,it3+it4=<2*A+ -3,it3+it4=<2*A+ -4,it3+it4=<2*A+ -5,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3=<2*A+ -3,it3=<2*A+ -4,it3=<2*A+ -5,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -3
            it7=<2/3*A+ -4/3,it7=<2/3*A+ -1,it7=<1/3*B+ -1/3,it7=<1/3*B+ -2/3,it6+it7=<2*A+ -3,it6+it7=<2*A+ -4,it6+it7=<1*B+ -1,it6+it7=<1*B+ -2,it6=<2*A+ -3,it6=<2*A+ -4,it6=<1*B+ -1,it6=<1*B+ -2
            it11=<2/3*A+ -4/3,it11=<2/3*A+ -7/3,it11=<2/3*A+ -1,it11=<2/3*A+ -2,it11=<1/3*B+ -1/3,it11=<1/3*B+ -2/3,it11=<1/3*B+ -4/3,it11=<1/3*B+ -5/3,it10+it11=<2*A+ -3,it10+it11=<2*A+ -4,it10+it11=<2*A+ -6,it10+it11=<2*A+ -7,it10+it11=<1*B+ -1,it10+it11=<1*B+ -2,it10+it11=<1*B+ -4,it10+it11=<1*B+ -5,it10=<2*A+ -3,it10=<2*A+ -4,it10=<2*A+ -6,it10=<2*A+ -7,it10=<1*B+ -1,it10=<1*B+ -2,it10=<1*B+ -4,it10=<1*B+ -5
            it14=<2/3*A+ -1,it14=<2/3*A+ -2,it14=<1/3*B+ -1/3,it14=<1/3*B+ -4/3,it13+it14=<2*A+ -3,it13+it14=<2*A+ -6,it13+it14=<1*B+ -1,it13+it14=<1*B+ -4,it13=<2*A+ -3,it13=<2*A+ -6,it13=<1*B+ -1,it13=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[72]: 5+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -3,it1+it2+it5=<1/2*B+ -2
            it4=<2/3*A+ -4/3,it4=<2/3*A+ -7/3,it4=<2/3*A+ -1,it4=<2/3*A+ -2,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<2*A+ -3,it3+it4=<2*A+ -4,it3+it4=<2*A+ -6,it3+it4=<2*A+ -7,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<2*A+ -3,it3=<2*A+ -4,it3=<2*A+ -6,it3=<2*A+ -7,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<2/3*A+ -1,it7=<2/3*A+ -2,it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<2*A+ -3,it6+it7=<2*A+ -6,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<2*A+ -3,it6=<2*A+ -6,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[73]: 6+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*A+ -4,it1=<2*A+ -3,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*A+ -4,it1+it2=<2*A+ -3,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*A+ -1,it2=<2/3*A+ -4/3,it3+it4+it7=<1*A+ -3,it3+it4+it7=<1/2*B+ -2
            it6=<2/3*A+ -4/3,it6=<2/3*A+ -7/3,it6=<2/3*A+ -1,it6=<2/3*A+ -2,it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<2*A+ -3,it5+it6=<2*A+ -4,it5+it6=<2*A+ -6,it5+it6=<2*A+ -7,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<2*A+ -3,it5=<2*A+ -4,it5=<2*A+ -6,it5=<2*A+ -7,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<2/3*A+ -1,it9=<2/3*A+ -2,it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<2*A+ -3,it8+it9=<2*A+ -6,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<2*A+ -3,it8=<2*A+ -6,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[74]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<2*A+ -4,it1=<2*A+ -3,it1=<2*B+ -2,it1=<2*B+ -1,it1=<4*A+ -6,it1=<4*A+ -5,it1+it2=<1*B+ -2,it1+it2=<1*B+ -1,it1+it2=<2*A+ -4,it1+it2=<2*A+ -3,it1+it2=<2*B+ -2,it1+it2=<2*B+ -1,it1+it2=<4*A+ -6,it1+it2=<4*A+ -5,it2=<1/3*B+ -2/3,it2=<1/3*B+ -1/3,it2=<2/3*A+ -1,it2=<2/3*A+ -4/3,it2=<2/3*B+ -2/3,it2=<2/3*B+ -1/3,it2=<4/3*A+ -2,it2=<4/3*A+ -5/3,it3+it4+it7=<1*A+ -3,it3+it4+it7=<1/2*B+ -2
            it6=<2/3*A+ -4/3,it6=<2/3*A+ -7/3,it6=<2/3*A+ -1,it6=<2/3*A+ -2,it6=<1/3*B+ -1/3,it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -5/3,it5+it6=<2*A+ -3,it5+it6=<2*A+ -4,it5+it6=<2*A+ -6,it5+it6=<2*A+ -7,it5+it6=<1*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -4,it5+it6=<1*B+ -5,it5=<2*A+ -3,it5=<2*A+ -4,it5=<2*A+ -6,it5=<2*A+ -7,it5=<1*B+ -1,it5=<1*B+ -2,it5=<1*B+ -4,it5=<1*B+ -5
            it9=<2/3*A+ -1,it9=<2/3*A+ -2,it9=<1/3*B+ -1/3,it9=<1/3*B+ -4/3,it8+it9=<2*A+ -3,it8+it9=<2*A+ -6,it8+it9=<1*B+ -1,it8+it9=<1*B+ -4,it8=<2*A+ -3,it8=<2*A+ -6,it8=<1*B+ -1,it8=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[75]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*A+ -3,it1+it2+it5=<1/2*B+ -2
            it4=<2/3*A+ -4/3,it4=<2/3*A+ -7/3,it4=<2/3*A+ -1,it4=<2/3*A+ -2,it4=<1/3*B+ -1/3,it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -5/3,it3+it4=<2*A+ -3,it3+it4=<2*A+ -4,it3+it4=<2*A+ -6,it3+it4=<2*A+ -7,it3+it4=<1*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -4,it3+it4=<1*B+ -5,it3=<2*A+ -3,it3=<2*A+ -4,it3=<2*A+ -6,it3=<2*A+ -7,it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*B+ -4,it3=<1*B+ -5
            it7=<2/3*A+ -1,it7=<2/3*A+ -2,it7=<1/3*B+ -1/3,it7=<1/3*B+ -4/3,it6+it7=<2*A+ -3,it6+it7=<2*A+ -6,it6+it7=<1*B+ -1,it6+it7=<1*B+ -4,it6=<2*A+ -3,it6=<2*A+ -6,it6=<1*B+ -1,it6=<1*B+ -4
  with precondition: [2*A=B+2,A>=4] 

eval1(A,B,C,D):[76]: 7+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it2=<1,it2=<2
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=3,B=4] 

eval1(A,B,C,D):[77]: 5+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it2=<1,it2=<2
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=3,B=4] 

eval1(A,B,C,D):[78]: 5+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))
  Such that:it1=<1,it1=<2,it1=<3,it1=<4,it1=<5,it1=<6,it1=<7,it1=<9,it1+it2=<1,it1+it2=<2,it1+it2=<3,it1+it2=<4,it1+it2=<5,it1+it2=<6,it1+it2=<7,it1+it2=<9,it2=<1,it2=<2,it2=<3,it2=<1/3,it2=<2/3,it2=<4/3,it2=<5/3,it2=<7/3,it3+it4=<1,it3+it4=<2,it4=<1
            it6=<2/3,it6=<1,it5+it6=<3,it5+it6=<2,it5=<3,it5=<2
  with precondition: [A=3,B=4] 

eval1(A,B,C,D):[79]: 6+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it2=<1,it2=<2
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=3,B=4] 

eval1(A,B,C,D):[80]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))
  Such that:it1+it2=<2,it1+it2=<3,it2=<1,it2=<2,it2=<3
            it4=<2/3,it4=<1,it3+it4=<3,it3+it4=<2,it3=<3,it3=<2
  with precondition: [A=3,B=4] 

eval1(A,B,C,D):[81]: 5
  with precondition: [2*A=B+2,A>=3] 

eval1(A,B,C,D):[82]: 6+it1*(1)+it2*(1)
  Such that:it1=<2,it1=<3,it1+it2=<2,it1+it2=<3,it2=<1,it2=<2/3
  with precondition: [A=3,B=4] 

eval1(A,B,C,D):[83]: 5+it1*(1)+it2*(1)
  Such that:it1=<2,it1=<2*A,it1=<1*B+ -1,it1=<1*B+2,it1=<2*A+ -3,it1=<2*B+ -1,it1=<4*A+ -5,it1+it2=<2,it1+it2=<2*A,it1+it2=<1*B+ -1,it1+it2=<1*B+2,it1+it2=<2*A+ -3,it1+it2=<2*B+ -1,it1+it2=<4*A+ -5,it2=<2/3*A,it2=<1/3*B+ -1/3,it2=<1/3*B+2/3,it2=<2/3*A+ -1,it2=<2/3*B+ -1/3,it2=<4/3*A+ -5/3,it2=<2/3
  with precondition: [2*A=B+2,A>=3] 

eval1(A,B,C,D):[84]: 4
  with precondition: [2*A=B+2,A>=3] 

eval1(A,B,C,D):[85]: 4
  with precondition: [A=2,B=2] 

eval1(A,B,C,D):[86]: 2
  with precondition: [1>=A,B>=3] 

eval1(A,B,C,D):[87]: 3+it1*(1)+it2*(1)
  Such that:it1=<1*B+ -2,it1=<1*B+ -2*A+ -1,it1+it2=<1*B+ -2,it1+it2=<1*B+ -2*A+ -1,it2=<1/3*B+ -2/3,it2=<1/3*B+ -2/3*A+ -1/3
  with precondition: [1>=A,2*A>=1,B>=4*A+1] 

eval1(A,B,C,D):[88]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*B+ -2,it1=<2*B+ -3,it1=<1*B+ -2*A+ -1,it1=<2*B+ -2*A+ -2,it1+it2=<1*B+ -2,it1+it2=<2*B+ -3,it1+it2=<1*B+ -2*A+ -1,it1+it2=<2*B+ -2*A+ -2,it2=<1/3*B+ -2/3,it2=<2/3*B+ -1,it2=<1/3*B+ -2/3*A+ -1/3,it2=<2/3*B+ -2/3*A+ -2/3
  with precondition: [1>=A,2*A>=1,B>=2*A+2] 

eval1(A,B,C,D):[89]: 3
  with precondition: [A=1,B=3] 

eval1(A,B,C,D):[90]: 1
  with precondition: [1>=A] 

eval1(A,B,C,D):[91]: 4+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -3,it2=<1*B+ -5,it2=<1*B+ -3,it5=<1*B+ -4,it5=<1*B+ -3
            it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3+it4=<1*B+ -4,it3=<1*B+ -2,it3=<1*B+ -3,it3=<1*B+ -4
            it7=<1/3*B+ -2/3,it7=<1/3*B+ -1,it6+it7=<1*B+ -2,it6+it7=<1*B+ -3,it6=<1*B+ -2,it6=<1*B+ -3
  with precondition: [A=1,B>=4] 

eval1(A,B,C,D):[92]: 2+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -3,it2=<1*B+ -5,it2=<1*B+ -3,it5=<1*B+ -4,it5=<1*B+ -3
            it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3+it4=<1*B+ -4,it3=<1*B+ -2,it3=<1*B+ -3,it3=<1*B+ -4
            it7=<1/3*B+ -2/3,it7=<1/3*B+ -1,it6+it7=<1*B+ -2,it6+it7=<1*B+ -3,it6=<1*B+ -2,it6=<1*B+ -3
  with precondition: [A=1,B>=4] 

eval1(A,B,C,D):[93]: 3+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -3,it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it4=<1*B+ -3,it1+it2+it4=<1*B+ -2,it1+it2+it7=<1*B+ -3,it1+it2+it7=<1*B+ -2,it1+it3+it4+it7=<1*B+ -3,it1+it3+it4+it7=<1*B+ -2,it1+it4=<1*B+ -3,it1+it4=<1*B+ -2,it1+it7=<1*B+ -3,it1+it7=<1*B+ -2,it2+it3+it4+it7=<1*B+ -4,it2+it3+it4+it7=<1*B+ -13/3,it2+it4=<1*B+ -4,it2+it4=<1*B+ -13/3,it2+it7=<1*B+ -4,it2+it7=<1*B+ -13/3,it3+it4+it7=<1*B+ -3,it4=<1*B+ -5,it7=<1*B+ -4
            it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5+it6=<1*B+ -4,it5=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -4
            it9=<1/3*B+ -2/3,it9=<1/3*B+ -1,it8+it9=<1*B+ -2,it8+it9=<1*B+ -3,it8=<1*B+ -2,it8=<1*B+ -3
  with precondition: [A=1,B>=6] 

eval1(A,B,C,D):[94]: 2+it1*(1)+it2*(1)+it3*(3)+it4*(3+it5*(1)+it6*(1))+it7*(3+it8*(1)+it9*(1))
  Such that:it1+it2+it3+it4+it7=<1*B+ -3,it1+it2+it3+it4+it7=<1*B+ -2,it1+it2+it3+it4+it7=<2*B+ -5,it1+it2+it3+it4+it7=<2*B+ -4,it1+it2+it4=<1*B+ -3,it1+it2+it4=<1*B+ -2,it1+it2+it4=<2*B+ -5,it1+it2+it4=<2*B+ -4,it1+it2+it7=<1*B+ -3,it1+it2+it7=<1*B+ -2,it1+it2+it7=<2*B+ -5,it1+it2+it7=<2*B+ -4,it1+it3+it4+it7=<1*B+ -3,it1+it3+it4+it7=<1*B+ -2,it1+it3+it4+it7=<2*B+ -5,it1+it3+it4+it7=<2*B+ -4,it1+it4=<1*B+ -3,it1+it4=<1*B+ -2,it1+it4=<2*B+ -5,it1+it4=<2*B+ -4,it1+it7=<1*B+ -3,it1+it7=<1*B+ -2,it1+it7=<2*B+ -5,it1+it7=<2*B+ -4,it2+it3+it4+it7=<1*B+ -11/3,it2+it3+it4+it7=<1*B+ -10/3,it2+it3+it4+it7=<1*B+ -8/3,it2+it3+it4+it7=<1*B+ -7/3,it2+it4=<1*B+ -11/3,it2+it4=<1*B+ -10/3,it2+it4=<1*B+ -8/3,it2+it4=<1*B+ -7/3,it2+it7=<1*B+ -11/3,it2+it7=<1*B+ -10/3,it2+it7=<1*B+ -8/3,it2+it7=<1*B+ -7/3,it3+it4+it7=<1*B+ -3,it4=<1*B+ -5,it7=<1*B+ -4
            it6=<1/3*B+ -2/3,it6=<1/3*B+ -4/3,it6=<1/3*B+ -1,it5+it6=<1*B+ -2,it5+it6=<1*B+ -3,it5+it6=<1*B+ -4,it5=<1*B+ -2,it5=<1*B+ -3,it5=<1*B+ -4
            it9=<1/3*B+ -2/3,it9=<1/3*B+ -1,it8+it9=<1*B+ -2,it8+it9=<1*B+ -3,it8=<1*B+ -2,it8=<1*B+ -3
  with precondition: [A=1,B>=5] 

eval1(A,B,C,D):[95]: 3+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -3,it2=<1*B+ -5,it2=<1*B+ -3,it5=<1*B+ -4,it5=<1*B+ -3
            it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3+it4=<1*B+ -4,it3=<1*B+ -2,it3=<1*B+ -3,it3=<1*B+ -4
            it7=<1/3*B+ -2/3,it7=<1/3*B+ -1,it6+it7=<1*B+ -2,it6+it7=<1*B+ -3,it6=<1*B+ -2,it6=<1*B+ -3
  with precondition: [A=1,B>=4] 

eval1(A,B,C,D):[96]: 1+it1*(3)+it2*(3+it3*(1)+it4*(1))+it5*(3+it6*(1)+it7*(1))
  Such that:it1+it2+it5=<1*B+ -3,it2=<1*B+ -5,it2=<1*B+ -3,it5=<1*B+ -4,it5=<1*B+ -3
            it4=<1/3*B+ -2/3,it4=<1/3*B+ -4/3,it4=<1/3*B+ -1,it3+it4=<1*B+ -2,it3+it4=<1*B+ -3,it3+it4=<1*B+ -4,it3=<1*B+ -2,it3=<1*B+ -3,it3=<1*B+ -4
            it7=<1/3*B+ -2/3,it7=<1/3*B+ -1,it6+it7=<1*B+ -2,it6+it7=<1*B+ -3,it6=<1*B+ -2,it6=<1*B+ -3
  with precondition: [A=1,B>=4] 

eval1(A,B,C,D):[97]: 4
  with precondition: [A=1,B=3] 

Solved cost expressions of eval1(A,B,C,D): 
eval1(A,B,C,D):[45]: 2  with precondition: [A>=2,B>=2] 
eval1(A,B,C,D):[46]: -2*A+1*B+5  with precondition: [A>=2,B+4>=4*A] 
eval1(A,B,C,D):[47]: -2*A+1*B+4  with precondition: [A>=2,B+1>=2*A] 
eval1(A,B,C,D):[48]: 3  with precondition: [2*A=B+2,A>=2] 
eval1(A,B,C,D):[49]: 1  with precondition: [A>=2] 
eval1(A,B,C,D):[50]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+4  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[51]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[52]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+3  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[53]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[54]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+3  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[55]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+1  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[56]: max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[57]: 1*B+ -2+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+3  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[58]: 1*B+ -2+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[59]: max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+1  with precondition: [A>=3,B+1>=2*A] 
eval1(A,B,C,D):[60]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+4  with precondition: [A=2,B>=3] 
eval1(A,B,C,D):[61]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+2  with precondition: [A=2,B>=3] 
eval1(A,B,C,D):[62]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+3  with precondition: [A=2,B>=5] 
eval1(A,B,C,D):[63]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+2  with precondition: [A=2,B>=4] 
eval1(A,B,C,D):[64]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+3  with precondition: [A=2,B>=3] 
eval1(A,B,C,D):[65]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+1  with precondition: [A=2,B>=3] 
eval1(A,B,C,D):[66]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+7  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[67]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[68]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+6  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[69]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[70]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+6  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[71]: max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+4  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[72]: max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[73]: 1*B+ -2+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+6  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[74]: 1*B+ -2+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[75]: max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+4  with precondition: [2*A=B+2,A>=4] 
eval1(A,B,C,D):[76]: 17  with precondition: [A=3,B=4] 
eval1(A,B,C,D):[77]: 15  with precondition: [A=3,B=4] 
eval1(A,B,C,D):[78]: 11  with precondition: [A=3,B=4] 
eval1(A,B,C,D):[79]: 16  with precondition: [A=3,B=4] 
eval1(A,B,C,D):[80]: 14  with precondition: [A=3,B=4] 
eval1(A,B,C,D):[81]: 5  with precondition: [2*A=B+2,A>=3] 
eval1(A,B,C,D):[82]: 8  with precondition: [A=3,B=4] 
eval1(A,B,C,D):[83]: 7  with precondition: [2*A=B+2,A>=3] 
eval1(A,B,C,D):[84]: 4  with precondition: [2*A=B+2,A>=3] 
eval1(A,B,C,D):[85]: 4  with precondition: [A=2,B=2] 
eval1(A,B,C,D):[86]: 2  with precondition: [1>=A,B>=3] 
eval1(A,B,C,D):[87]: -2*A+1*B+2  with precondition: [1>=A,2*A>=1,B>=4*A+1] 
eval1(A,B,C,D):[88]: -2*A+1*B+1  with precondition: [1>=A,2*A>=1,B>=2*A+2] 
eval1(A,B,C,D):[89]: 3  with precondition: [A=1,B=3] 
eval1(A,B,C,D):[90]: 1  with precondition: [1>=A] 
eval1(A,B,C,D):[91]: max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+4  with precondition: [A=1,B>=4] 
eval1(A,B,C,D):[92]: max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+2  with precondition: [A=1,B>=4] 
eval1(A,B,C,D):[93]: max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+3  with precondition: [A=1,B>=6] 
eval1(A,B,C,D):[94]: max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+2  with precondition: [A=1,B>=5] 
eval1(A,B,C,D):[95]: max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+3  with precondition: [A=1,B>=4] 
eval1(A,B,C,D):[96]: max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+1  with precondition: [A=1,B>=4] 
eval1(A,B,C,D):[97]: 4  with precondition: [A=1,B=3] 
Maximum cost of eval1(A,B,C,D): max([-2*A+1*B+5,17,max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+4,max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5,max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+1,max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2,max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+1,max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+2,max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+3,max([3*B+ -9, (1*B+ -3)* (1*B), (1*B+ -1)* (1*B+ -3)])+4,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+1,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+2,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+3,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+4,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+4,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+6,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+7,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+1,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+3,max([3*B+ -6, (1*B+ -2)* (1*B), (1*B+1)* (1*B+ -2)])+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+4,1*B+ -2+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+5,1*B+ -2+max([3*A+ -9, (1*B+ -2)* (1*A+ -3), (1*B+ -1)* (1*A+ -3)])+6,1*B+ -2+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+2,1*B+ -2+max([3*A+ -6, (1*B+ -2)* (1*A+ -2), (1*B+ -1)* (1*A+ -2)])+3]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 16 ms.
Invariants computed in 637 ms.
----Backward Invariants 465 ms.
----Transitive Invariants 16 ms.
Refinement performed in 214 ms.
Termination proved in 33 ms.
Upper bounds computed in 3555 ms.
----Phase cost structures 1653 ms.
--------Equation cost structures 1312 ms.
--------Inductive compression(1) 12 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 1678 ms.
----Solving cost expressions 171 ms.

Compressed phase information: 80 
Compressed Chains: 0 
Compressed invariants: 7 
Total analysis performed in 4489 ms.