Q1.What are the "standard" techniques (if any) used to prove that a set of vectors in $\mathbb{N}^k$ defined using a set of constraints among the components is (or is not) a semilinear set (i.e. a finite union of linear sets) ?

For example, given:

$A = \{ \langle x_1, x_2, x_3, x_4, x_5, x_6 \rangle \mid \sum_i x_i \equiv 0 \bmod 6 \land [x_1 + x_2 + x_3 \neq x_4+x_5+x_6] \land [(x_1 + x_2 \neq x_3 + x_4) \lor (x_3 + x_4 \neq x_5 + x_6) ]\} $

how can I (dis)prove that $A$ is semilinear?

Q2.Can this process be automated assuming that the conditions are given using a set of logic expressions with numeric constants and operators $\land, \lor, +, -, =, \neq, \leq$? And if it can be automated, what is its (computational) complexity?