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