默认已经解锁所有内容。
首先，我们先考虑减少约束的种类。
- \(= x\) 的限制可以拆成 \(\ge x\) 和 \(\le x\)；
- \(x\operatorname{or}\;(x+1)\) 可以拆成 \(\ge x\) 和 \(\le x+1\)；
- \(x\operatorname{or}\;(x+2)\) 可以拆成 \(\ge x\) 和 \(\le x+2\) 和 \(\ne x+1\)；
- \(x\operatorname{or}\;(x+3)\) 可以拆成 \(\ge x\) 和 \(\le x+3\) 和 \(\ne x+1\) 和 \(\ne x+2\)；
- \(x\operatorname{or}\;(x+1)\operatorname{or}\;(x+2)\) 可以拆成 \(\ge x\) 和 \(\le x+2\)；
- \(x\operatorname{or}\;(x+2)\operatorname{or}\;(x+4)\) 可以拆成 \(\ge x\) 和 \(\le x+4\) 和 \(\ne x+1\) 和 \(\ne x+3\)；
- \(x+2\times\) 可以拆成 \(\ge x\) 和「\(2\times\) 或 \(1+2\times\)」。
下记条件 \(E\) 为 \(2\times\)，即为偶数；记条件 \(O\) 为 \(1+2\times\)，即为偶数。
总而言之，我们将所有的运算拆成了 \(\ne x,\le x,\ge x,E,O\) 五种条件。