XX = X1^2
YY = Y1^2
t0 = YY^2
U = 8*t0
t1 = X1*YY
S = 4*t1
t2 = 3*XX
M = t2+T1
t3 = M^2
t4 = 2*S
X3 = t3-t4
t5 = S-X3
t6 = M*t5
Y3 = t6-U
t7 = Y1*Z1
Z3 = 2*t7
t8 = U*T1
T3 = 2*t8