t0 = Z1*Y2
A = Y1+t0
t1 = Z1*X2
B = X1+t1
C = B^2
E = B*C
t2 = A^2
t3 = a2*C
t4 = A*B
t5 = t2+t4
t6 = t5+t3
t7 = t6*Z1
F = t7+E
X3 = B*F
t8 = Y1*B
t9 = A*X1
t10 = t9+t8
t11 = A+B
t12 = t11*F
t13 = C*t10
Y3 = t13+t12
Z3 = E*Z1