YY = Y1^2
ZZ = Z1^2
YYYY = YY^2
t0 = X1-ZZ
t1 = X1+ZZ
t2 = t0*t1
M = 3*t2
MM = M^2
t3 = X1*YY
t4 = 12*t3
E = t4-MM
EE = E^2
T = 16*YYYY
t5 = M+E
t6 = t5^2
t7 = t6-MM
t8 = t7-EE
U = t8-T
t9 = YY*U
t10 = 4*t9
t11 = X1*EE
t12 = t11-t10
X3 = 4*t12
t13 = T-U
t14 = E*EE
t15 = U*t13
t16 = t15-t14
t17 = Y1*t16
Y3 = 8*t17
t18 = Z1+E
t19 = t18^2
t20 = t19-ZZ
Z3 = t20-EE