A = X2*X3
B = Z2*Z3
XX2 = X2^2
ZZ2 = Z2^2
t0 = sqrta6*ZZ2
t1 = XX2+t0
X4 = t1^2
Z4 = XX2*ZZ2
t2 = sqrta6*B
t3 = A+t2
X5 = t3^2
t4 = X2+Z2
t5 = X3+Z3
t6 = t4*t5
t7 = t6-A
t8 = t7-B
t9 = t8^2
Z5 = X1*t9