showHeuristics	=	False;
showproof = True;

triangcount =	0;
triangtrue =	0;

(* 1.1 *)
trineq[3*csum[a*b]<=csum[a]^2];
trineq[csum[a]^2<4*csum[a*b]];
(* 1.2 *)
trineq[csum[a^2]>=(36/35)*(s^2+a*b*c/s)];
(* 1.3 *)
trineq[8*cprod[s-a]<=a*b*c];
(* 1.4 *)
trineq[8*a*b*c<=cprod[a+b]];
(* 1.5 *)
trineq[3*cprod[a+b]<=8*csum[a^3]];
(* 1.6 *)
trineq[2*csum[a]*csum[a^2]>=3*(csum[a^3]+3*a*b*c)];
(* 1.7 *)
trineq[a*b*c<csum[a^2*(s-a)]];
trineq[csum[a^2*(s-a)]<=3*a*b*c/2];
(* 1.8 *)
trineq[csum[a*b*(a+b)]>=48*cprod[s-a]];
(* 1.9 *)
trineq[csum[a^3*(s-a)]<=a*b*c*s];
(* 1.10 *)
trineq[csum[a^5*(s-a)]<=(1/2)*a*b*c*csum[a^3]];
(* 1.11 *)
(*
trineq[csum[a^2*b*(a-b)]>=0];
*)
(* 1.12 *)
trineq[64*s^3*cprod[s-a]<=27*a^2*b^2*c^2];
(* 1.14 *)
trineq[2*s/(a*b*c)<=csum[1/a^2]];
(* 1.15 *)
trineq[csum[1/(s-a)]>=9/s];
(* 1.16 *)
trineq[3/2<=csum[a/(b+c)]];
trineq[csum[a/(b+c)]<2];
(* 1.17 *)
trineq[15/4<=csum[(s+a)/(b+c)]];
trineq[csum[(s+a)/(b+c)]<9/2];
(* 1.19 *)
trineq[1/3<=csum[a^2]/csum[a]^2];
trineq[csum[a^2]/csum[a]^2<1/2];
(* 1.22 *)
trineq[csum[a^2]*csum[b^3*c^3]<2*csum[a^5]*csum[a^3]];
(* 1.23 *)
trineq[csum[a]^3<=5*csum[a*b*(a+b)]-3*a*b*c];

Print[" "];
Print["Summary:"];
Print["Proved ",triangtrue," inequalities out of ",
	triangcount,"."];