t0 = Y1^2
t1 = X1*t0
S = 4*t1
t2 = X1^2
t3 = Z1^4
t4 = a*t3
t5 = 3*t2
M = t5+t4
t6 = M^2
t7 = 2*S
T = t6-t7
X3 = T
t8 = S-T
t9 = Y1^4
t10 = 8*t9
t11 = M*t8
Y3 = t11-t10
t12 = Y1*Z1
Z3 = 2*t12