t3 = Z2^2
t1 = X1 * t3
t4 = Z2 * t3
t3 = Y1 * t4
t4 = Z1^2
t2 = X2 * t4
t5 = Z1 * t4
t4 = Y2 * t5
t2 = t2 - t1
t4 = t4 - t3
t7 = t2^2
t6 = t1 * t7
t5 = t7 * t2
X = t4^2
X = X - t5
X = X - t6
X3 = X - t6
t6 = t6 - X3
Y = t4 * t6
t1 = t5 * t3
Y3 = Y - t1
t1 = Z1 * Z2
Z3 = t1 * t2