Questions:
Q1: Is there any intuition behind the following "ugly" identity? $$\forall x,y,z\in\mathbb{R},\text{if}\;x+y+z=0,\text{then}\;|x+|y|-z|+|x-y+|z||-x-2|x|-|y|-|z|=0$$ A more symmetrical form can be obtained by swapping and averaging but I don't see the necessity.
Q2: Given an expression involving only addition, subtraction and absolute value of real numbers, is there any quick way to verify whether it is identical to zero, instead of brutely checking all the possible outcomes of absolute values?
Q3: Would there be any mechanism able to generating all the identities involving only addition, subtraction and absolute value of real numbers, or at least some of them? For example, if we can lexically encode these expressions, we may be able to list one-by-one all the expressions and then pick out those which are identities...
Q4: It is easily to see its connection to the SAT problem, are they equivalent?
Background:
This question was inspired by the following function: $$f_r(v,w)=\max{(v-r,\min{(v+r,w}))},$$ where $r\in\mathbb{R}^+$ can be thought as the parameter of the function and $v,w\in\mathbb{R}$ are the two inputs. I was asked to check that $f_r(v,f_r(v,w))=f_r(v,w)$ and it was trivial. I noticed that $$\max{(a,\min{(b,w}))}-\min{(b,\max{(a,w}))}=\left\{\begin{aligned}&a-b,&a\geq b\\&0,&a<b\end{aligned}\right.$$ It is also easy to check this but when I rewrite the min/max function using absolute values, the identity seems less apparent.