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