Solving for $a,b,c,d$ where $a^2 + b^2 + c^2 + d^2 = 630^2$

Question

How could one solve for $a,b,c,d$ where:

$$a^2 + b^2 + c^2 + d^2 = 630^2,\ a>b>c>d$$

$a,b,c,d$ squared is equal to the square of $630$, and $a$ is larger than $b$, and so forth.

$a,b,c,d$ is also of such form that:

$$n = x + (x+1) + (x+2) + (x+3), \ x\in\mathbb{N}$$

where $n$ could be substituted for $ a, b, c \ $or $d$.

In what ways could one attack this problem?

Answer 1

I've asked the Z3 solver using the Python interface (a 2nd time ...):

a, b, c, d = Ints('a b c d')
ax, bx, cx, dx = Ints('ax bx cx dx')

solve(a*a + b*b + c*c + d*d == 630*630,
      a > b,
      b > c,
      c > d,
      a == 4*ax + 6,
      b == 4*bx + 6,
      c == 4*cx + 6,
      d == 4*dx + 6,
      show=True)

Solution:

timed out, probably no solution

Answer 2

Since $a, b, c, d$ are all of the form $4x+6$ for some $x \in \mathbb{N}$, we see that $a,b,c,d \equiv 2 \pmod 4$. It follows that $a^2+b^2+c^2+d^2 \equiv 4+4+4+4 \equiv 0 \pmod 8$. However, $630^2 \equiv 4 \pmod 8$. Therefore there is no solution.