A = X1*Z2
B = Z1*Z2
C = Y1*X2
D = Y1*Y2
E = Z1*Y2
t0 = X1*X2
F = a*t0
t1 = C*D
t2 = A*B
X3 = t2-t1
t3 = F*A
t4 = D*E
Y3 = t4-t3
t5 = B*E
t6 = F*C
Z3 = t6-t5