这题其实就是EUF(Equality and Uninterpreted Functions，等式与未解释函数)理论中Equality那部分，出题人绝对也是业内人士！！题中的等号/不等号两侧可以是任何东西：一个bool变量，一个大到CE的数组，一只猫咪，一个可爱的美少女原OIer……求解器不知道这些具体是什么，只能通过用户提供的等和不等约束来做推理：

• $a = b \wedge b = c \rightarrow a = c$ （传递性）
• $\neg (a = b \wedge a \neq b)$ （不能既等又不等）

在很多求解器中，这部分推理就是用并查集实现的，大家已经在本题中体验过了。（作为一个先去实验室打工才回来学OI的老蒟蒻，我就是通过EUF才知道的并查集）

本题没有提到的部分是Uninterpreted Functions。同样，函数$f$也可以是任何东西（比如$f(x)$表示物体的腿数，$f(人)=2$，$f(桌子)=4$）求解器把这样的函数完全当作黑盒，只知道如果参数相等，那么返回值相等（推理出结果同样可以使用并查集来维护）：

$x_1 = x_2 \wedge y_1 = y_2 \wedge \cdots \rightarrow f(x_1, y_1, \cdots) = f(x_2, y_2, \cdots)$

那么这个EUF到底有什么用呢？倒不真研究物体的腿数，而是研究sinx这样的非线性函数。目前约束求解机能有限，很难把sinx这种复杂函数当作白盒处理，作为补救，知道$x = y \rightarrow sinx = siny$这样的小结论也能解决一部分问题。