t0 = X1^2
t1 = X1*t0
U = a*t1
t2 = Y1^2
V = Y1*t2
t3 = Z1^2
W = Z1*t3
t4 = U-V
A = t4^2
t5 = U-W
B = t5^2
t6 = V-W
C = t6^2
D = A+C
E = A+B
t7 = U+V
t8 = t7+W
t9 = B+D
t10 = t8*t9
X3 = recipd*t10
t11 = C-E
t12 = V*t11
t13 = U*C
t14 = 2*t13
Y3 = t14-t12
t15 = B-D
t16 = U*t15
t17 = V*B
t18 = 2*t17
Z3 = t18-t16