A = X2*X3
B = Z2*Z3
t0 = A^2
t1 = B^2
t2 = a6*t1
t3 = t0+t2
X5 = Z1*t3
t4 = X2+Z2
t5 = X3+Z3
t6 = t4*t5
t7 = t6-A
t8 = t7-B
t9 = t8^2
Z5 = X1*t9