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 t4 = t3^2 X5 = Z1*t4 t5 = X2+Z2 t6 = X3+Z3 t7 = t5*t6 t8 = t7-A t9 = t8-B t10 = t9^2 Z5 = X1*t10