8*x2^4*x5^4 + 8*x2^2*x3^2*x5^4 + 2*x3^4*x5^4 + 2*x2^2*x4^2*x5^4 + x3^2*x4^2*x5^4 + 8*x2^4*x5^2*x6^2 + 4*x2^2*x3^2*x5^2*x6^2 + x2^2*x4^2*x5^2*x6^2 + 2*x2^4*x6^4 + 2*x2^4*x5^2*x7^2 + x2^2*x3^2*x5^2*x7^2 + x2^4*x6^2*x7^2 + 20*x1*x2^4*x5^2 + 24*x1*x2^2*x3^2*x5^2 + 8*x1*x3^4*x5^2 + 4*x1*x2^2*x4^2*x5^2 + 4*x1*x3^2*x4^2*x5^2 + 20*x0*x2^2*x5^4 + 8*x0*x3^2*x5^4 + 8*x1*x2^4*x6^2 + 4*x1*x2^2*x3^2*x6^2 + 24*x0*x2^2*x5^2*x6^2 + 4*x0*x3^2*x5^2*x6^2 + 8*x0*x2^2*x6^4 + 4*x0*x2^2*x5^2*x7^2 + 4*x0*x2^2*x6^2*x7^2 + 14*x1^2*x2^4 + 20*x1^2*x2^2*x3^2 + 8*x1^2*x3^4 + 2*x1^2*x2^2*x4^2 + 4*x1^2*x3^2*x4^2 + 52*x0*x1*x2^2*x5^2 + 28*x0*x1*x3^2*x5^2 + 14*x0^2*x5^4 + 28*x0*x1*x2^2*x6^2 + 8*x0*x1*x3^2*x6^2 + 20*x0^2*x5^2*x6^2 + 8*x0^2*x6^4 + 2*x0^2*x5^2*x7^2 + 4*x0^2*x6^2*x7^2 + 36*x0*x1^2*x2^2 + 24*x0*x1^2*x3^2 + 36*x0^2*x1*x5^2 + 24*x0^2*x1*x6^2 + 24*x0^2*x1^2 - 1/(2^32)