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