Is $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ provable in MLL?

Question

Consider the multiplicative fragment of linear logic (MLL) which only consists of the multiplicative connectives tensor and par together with the inference rules axiom, cut, $\otimes$ and ⅋. I was able to show that $(A⅋B) \otimes C \vdash A ⅋ (B \otimes C) $ holds. Is the other entailment $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ also provable in MLL? I could not come up with a proof.

Answer 1

The axioms and rules of MLLL are valid in classical logic if we read tensor as $\land$ and par as $\lor$. Since $A\lor(B\land C)$ doesn't classically imply $(A\lor B)\land C$, MLL doesn't prove your sequent.