t0 = X1*Z1
t1 = t0+Y1
U1 = t1^2
U2 = Y1^2
t2 = X1^2
V1 = t2^2
t3 = X1*Z1
S1 = t3^2
t4 = a2*S1
t5 = U2-V1
T = t5-t4
t6 = U1-U2
X3 = t6-S1
t7 = a2*S1
t8 = T+V1
t9 = U2+t7
t10 = S1^2
t11 = 4*t10
t12 = t8*t9
Y3 = t12+t11
Z3 = T-V1