Batchload(Inequal)$ /* */ showproof: true $ test(x^2+y^2>=2*x*y); test(x^3*y+x*y^3<=x^4+y^4); test((x+y)*(y+z)*(z+x)>=8*x*y*z); test(4*(x^3+y^3)>=(x+y)^3); test((x+y+z)^3>=27*x*y*z); test(x*y*z>=(x+y-z)*(y+z-x)*(z+x-y)); test(x^2*(1+y^2)+y^2*(1+z^2)+z^2*(1+x^2)>=6*x*y*z); test(8*(x^3+y^3+z^3)^2>=9*(x^2+y*z)*(y^2+z*x)*(z^2+x*y)); test(4*(x^5+y^5+z^5+w^5)>=(x^3+y^3+z^3+w^3)*(x^2+y^2+z^2+w^2)); test((b+c+d)*(c+d+a)*(d+a+b)*(a+b+c)>=81*a*b*c*d); test((x^2*y+y^2*z+z^2*x)*(x*y^2+y*z^2+z*x^2)>=9*x^2*y^2*z^2); test(6*x*y*z<=x*y*(x+y)+y*z*(y+z)+z*x*(z+x)); test(x^2*y^2+y^2*z^2+z^2*x^2>=x*y*z*(x+y+z)); test((x+y+z)^3>=(x+y-z)*(y+z-x)*(z+x-y)); test(27*(x^4+y^4+z^4)>=(x+y+z)^4); test((x+y+z+w)*(x^3+y^3+z^3+w^3)>=(x^2+y^2+z^2+w^2)^2); test(x*(x-y)*(x-z)+y*(y-z)*(y-x)+z*(z-x)*(z-y)>=0); test(x^2*(x-y)*(x-z)+y^2*(y-z)*(y-x)+z^2*(z-x)*(z-y)>=0); test(x^5*(x-y)*(x-z)+y^5*(y-z)*(y-x)+z^5*(z-x)*(z-y)>=0); test(9*(x^6+y^6+z^6)>=(x^3+y^3+z^3)*(x^2+y^2+z^2)*(x+y+z)); test(16*(x^3+y^3+z^3+w^3)>=(x+y+z+w)^3); test((x+y-z)^2+(y+z-x)^2+(z+x-y)^2>=x*y+y*z+z*x); test(x^3+y^3+z^3+3*x*y*z>=x^2*(y+z)+z^2*(x+y)+y^2*(z+x)); test(6*x*y*z<=x^2*(y+z)+y^2*(z+x)+z^2*(x+y)); test(x^2*(y+z)+y^2*(z+x)+z^2*(x+y)<=2*(x^3+y^3+z^3)); test(a*b*c*d>=(b+c+d-2*a)*(c+d+a-2*b)*(d+a+b-2*c)*(a+b+c-2*d)); test(3*(x^2*y+y^2*z+z^2*x)*(x*y^2+y*z^2+z*x^2)>=x*y*z*(x+y+z)^3); test((x^3+y^3)^2<=(x^2+y^2)^3); test((x^7+y^7)^3<=(x^3+y^3)^7); test(1/x+1/y+1/z>=9/(x+y+z)); test(x/(y+z)+y/(z+x)+z/(x+y)>=3/2); test(x^(-5)*(x-y)*(x-z)+y^(-5)*(y-z)*(y-x)+z^(-5)*(z-x)*(z-y)>=0); test(1/x+1/y+1/z<=(x^8+y^8+z^8)/(x^3*y^3*z^3)); test(1/(x+y+z)+1/(y+z+w)+1/(z+w+x)+1/(w+x+y)>=(16/3)/(x+y+z+w)); test((x^2+y^2)/(x+y)+(y^2+z^2)/(y+z)+(z^2+x^2)/(z+x)>=x+y+z); test((a^3+b^3+c^3+d^3+e^3)*(1/a+1/b+1/c+1/d+1/e)>=5*(a^2+b^2+c^2+d^2+e^2)); test(3/(b+c+d)+3/(c+d+a)+3/(d+a+b)+3/(a+b+c)>=16/(a+b+c+d));