t0 = X2^2 t1 = Z2^2 t2 = a*t1 t3 = t0-t2 t4 = t3^2 t5 = Z2^3 t6 = X2*t5 t7 = b*t6 t8 = 8*t7 X4 = t4-t8 t9 = X2^2 t10 = Z2^2 t11 = a*t10 t12 = t9+t11 t13 = Z2^4 t14 = b*t13 t15 = Z2*t12 t16 = X2*t15 t17 = t16+t14 Z4 = 4*t17 t18 = Z2*Z3 t19 = a*t18 t20 = X2*X3 t21 = X3*Z2 t22 = X2*Z3 t23 = t22+t21 t24 = t20+t19 t25 = Z2^2 t26 = Z3^2 t27 = t25*t26 t28 = b*t27 t29 = 4*t28 t30 = t23*t24 t31 = 2*t30 R = t31+t29 t32 = X3*Z2 t33 = X2*Z3 t34 = t33-t32 S = t34^2 t35 = S*X1 X5 = R-t35 Z5 = S