YY1 = Y1^2
t0 = 3*ZZ1
t1 = X1+t0
A = t1^2
t2 = ZZ1*A
B = a*t2
Xt = YY1+B
t3 = 3*B
t4 = YY1-t3
Yt = Y1*t4
Zt = X1*Z1
C = Zt^2
Ca = a*C
t5 = 9*C
t6 = 4*Ca
t7 = t6-t5
t8 = t7-Xt
t9 = t8^2
t10 = Ca*t9
E = 3*t10
t11 = Yt^2
X3 = t11-E
t12 = 4*E
t13 = X3+t12
Y3 = Yt*t13
t14 = Xt*Zt
Z3 = 3*t14
ZZ3 = Z3^2