An inequality concerning formulas and Boolean functions We define $S(\phi)$ of formula $\phi$ to be the number of computational gates in a minimal $\{\neg, \wedge, \vee\}$-formula computing $\phi$.
Conjecture. If $\phi_1(a_{11}, \dots, a_{1y_1})$, $\dots$, $\phi_x(a_{x1}, \dots, a_{xy_x})$ are arbitrary Boolean functions with pairwise disjoint sets of variables, then it follows that$$S\left(\phi_1\left(a_{11}, \dots, a_{1y_1}\right) \oplus \ldots \oplus \phi_x\left(a_{x1}, \dots, a_{xy_x}\right)\right) \ge {1\over2}\sum_{i = 1}^x S(\phi_i).$$Is this true or not? If so, how do we show this? Or does there exist a counterexample?
 A: EDIT: the strikethroughs are in response to the followup comments that ensued.
I believe this is open.  For simplicity, assume the $\phi$'s are the same function.  It's a bit more standard to write $L(\phi)$ for the minimum formula size of $\phi$.  The original question is whether $L(\oplus_m \circ f) \gtrapprox m L(f)$, where $\oplus_m$ denotes arity-$m$-XOR.  Indeed, one could hope even for $L(\oplus_m \circ f) \gtrapprox m^2 L(f)$, since the formula complexity of $\oplus_m$ is $m^2$.
This stronger (potential) lower bound is presented as a major conjecture (Conjecture 1.10) in the following recent work of Gavinsky, Meir, Weinstein, and Wigderson: http://www.math.ias.edu/~avi/PUBLICATIONS/GavinskyMeWeWi2016.pdf  The question dates back to Karchmer-Raz-Wigderson'95.
This leaves open the weaker statement $L(\oplus_m \circ f) \gtrapprox m L(f)$ -- basically, what was asked in the original question -- but my guess is that this is equally unknown.
One more remark: as noted in the paper above, the desired conjecture is true if the XOR operation is replaced by the OR operation.
EDIT: Wegener's observation (see coments) that the desired conjecture holds true for OR seems to apply equally well for XOR, as noted by Fedja.  So it would seem that the answer to the poster's question is positive, even without the factor $1/2$, assuming the $\phi$'s are nonconstant.
A: Edit As Emil pointed out, that will work for the circuit complexity, but not for the formula complexity. I apologize for being confused, but still will leave this post just as a curious observation.
Here is a possible candidate for an (interesting) counterexample.
Take some big $y$ and a prime $p$ slightly bigger than $2^y$. Let all $\varphi_j$ be the same and return $0$ if the binary number $\overline{a_1\dots a_y}+1$ is a quadratic residue modulo $p$ and $1$ otherwise.
Let $M$ be the complexity of $\varphi$ and $m$ be the complexity of arithmetic operations (addition and multiplication) modulo $p$. 
Religious dogma: When $y$ is large, $M/m$ is also large.
If we believe it, then the composite formula can be computed by first multiplying all numbers out, subtracting $1$ and then applying $\varphi$, thus consuming only about $xm+M\ll xM$ gates.
My question is whether we can set up some construction like that staying purely within mathematics. 
A: I'm not sure what you mean by $\oplus$, but here is a counterexample. Let each $\phi_i(\vec x)$ be a tautology. So $S(\phi_i)=2$. But $\phi_1\oplus\cdots\phi_x$ is also trivial (depending on what you mean by $\oplus$), and so takes just a few operations. But $\frac12\sum_i S(\phi_i)=x$, which can be very large. 
