t0 = XX1+ZZ1
t1 = 2*t0
t2 = XY1-YZ1
t3 = XZ1+t1
X3 = t2*t3
t4 = YY1+ZZ1
t5 = 2*t4
t6 = XZ1-XY1
t7 = YZ1+t5
Y3 = t6*t7
t8 = XX1+YY1
t9 = 2*t8
t10 = YZ1-XZ1
t11 = XY1+t9
Z3 = t10*t11
XX3 = X3^2
YY3 = Y3^2
ZZ3 = Z3^2
t12 = X3+Y3
t13 = t12^2
t14 = t13-XX3
XY3 = t14-YY3
t15 = X3+Z3
t16 = t15^2
t17 = t16-XX3
XZ3 = t17-ZZ3
t18 = Y3+Z3
t19 = t18^2
t20 = t19-YY3
YZ3 = t20-ZZ3