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