For finite multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, where $\uplus$ denotes mutliset sum as defined here https://oeis.org/wiki/Multisets#Multiset_sum
EDIT: Here's why I'm interested in this question. In simply relationally typed higher-order languages following Orey "Model Theory for the Higher Order Predicate Calculus" (1959), predicates have different syntactic types, which are identified with sequences of types. The idea is that, if a predicate is of type $\langle t_1,\dots,t_n\rangle$, then it combines with $n$ arguments respectively of types $t_1,\dots,t_n$ in that order to form a formula. I'm interested in how to think about higher-order languages like this except where, intuitively, the argument-places of predicates are unordered; to form a formula by combining a predicate with some arguments you can't just list the arguments -- instead (simplifying somewhat) you biject arguments with argument-places of the predicate. In this framework, types of predicates aren't identified with sequences of types, but with multisets of types, since multisets are basically unordered sequences.
The reason I'm interested in the particular equation above is that, in thinking about how to do combinatory logic in such a higher-order language, it turns out that the analogue of what are usually called B combinators end up having types of the above form, and I'm interested in whether these combinators, in this setting, are uniquely determined by their types, or whether there could be distinct B-like combinators of the same type. (Intuitively, such a combinator of type $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ can combine with arguments $a_1,...,a_n$ the multiplicity of the types of which is $A$, $b_1,...,b_m$ the multiplicity of the types of which is $B$, a predicate of type $\{B \uplus C\}$, and a predicate of type $\{A \uplus \{C\}\}$ to form a formula. For example, if $A=B=C=\{e\}$ (where $e$ is the base type of individuals), the relevant B-like combinator will be analogous to the simply relationally-typed lambda-term $\beta := (\lambda x^ey^eX^{\langle e,e\rangle}Y^{\langle e,\langle e\rangle\rangle}.Yx(\lambda z^e.Xyz))$, which combines with terms $a$ and $b$ of type $e$, a predicate $R$ of type $\langle e,e\rangle$, and a predicate $S$ of type $\langle e, \langle e\rangle\rangle$, to form a formula $\beta abRS$ which we can think of as saying that individual $a$ stands in relation $S$ to the property of being $R$-related to individual $b$.)
Maybe this is still too random a question to count as research-level for the purposes of this site, but I thought I'd add this explanation to indicate that it is at least a question that arose in the course of research, and isn't just a homework assignment or something.
