\ Equation counts \ Total E G L N X C B \ 209 4 179 26 0 0 0 0 \ \ Variable counts \ x b i s1s s2s sc si \ Total cont binary integer sos1 sos2 scont sint \ 17 17 0 0 0 0 0 0 \ \ Nonzero counts \ Total const NL DLL \ 1264 176 1088 0 \ Minimize obj: x2 + 0 x3 + 0 x4 + 0 x5 + 0 x6 + 0 x7 + 0 x8 + 0 x9 + 0 x10 + 0 x11 + 0 x12 + 0 x13 + 0 x14 + 0 x15 + 0 x16 + 0 x17 + 0 x18 Subject To e2: 0.20410502 x3 + 2.24629156 x4 - x5 <= 0 e3: 3.94678752 x6 - 1.42893791 x7 - x8 <= 0 e4: - 1.52786255 x9 + 2.47212728 x10 - x11 <= 0 e5: 0.43022284 x12 + 1.63415571 x13 - x14 <= 0 e6: 3.40502701 x3 - 1.59481484 x4 - x5 <= 0 e7: - 6.05321248 x6 - 1.42893791 x7 - x8 <= 0 e8: 2.47213745 x9 + 0.47212728 x10 - x11 <= 0 e9: 1.60415853 x12 - 1.04912586 x13 - x14 <= 0 e10: - 4.40522266 x3 - 1.59481484 x4 - x5 <= 0 e11: 0.19678752 x6 + 1.69606209 x7 - x8 <= 0 e12: 3.47213745 x9 - 1.52787272 x10 - x11 <= 0 e13: - 3.14748592 x12 - 1.04912586 x13 - x14 <= 0 e14: - 1.52786255 x9 - 1.52787272 x10 - x11 <= 0 e15: x2 + 0.20410502 x3 + 2.24629156 x4 - x5 >= 0 e16: x2 + 3.94678752 x6 - 1.42893791 x7 - x8 >= 0 e17: x2 - 1.52786255 x9 + 2.47212728 x10 - x11 >= 0 e18: x2 + 0.43022284 x12 + 1.63415571 x13 - x14 >= 0 e19: x2 + 3.40502701 x3 - 1.59481484 x4 - x5 >= 0 e20: x2 - 6.05321248 x6 - 1.42893791 x7 - x8 >= 0 e21: x2 + 2.47213745 x9 + 0.47212728 x10 - x11 >= 0 e22: x2 + 1.60415853 x12 - 1.04912586 x13 - x14 >= 0 e23: x2 - 4.40522266 x3 - 1.59481484 x4 - x5 >= 0 e24: x2 + 0.19678752 x6 + 1.69606209 x7 - x8 >= 0 e25: x2 + 3.47213745 x9 - 1.52787272 x10 - x11 >= 0 e26: x2 - 3.14748592 x12 - 1.04912586 x13 - x14 >= 0 e27: x2 - x5 >= 0 e28: x2 - x8 >= 0 e29: x2 - 1.52786255 x9 - 1.52787272 x10 - x11 >= 0 e30: x2 - x14 >= 0 e31: - 2.24629156 x3 + 0.20410502 x4 - x15 <= 0 e32: 1.42893791 x6 + 3.94678752 x7 - x16 <= 0 e33: - 2.47212728 x9 - 1.52786255 x10 - x17 <= 0 e34: - 1.63415571 x12 + 0.43022284 x13 - x18 <= 0 e35: 1.59481484 x3 + 3.40502701 x4 - x15 <= 0 e36: 1.42893791 x6 - 6.05321248 x7 - x16 <= 0 e37: - 0.47212728 x9 + 2.47213745 x10 - x17 <= 0 e38: 1.04912586 x12 + 1.60415853 x13 - x18 <= 0 e39: 1.59481484 x3 - 4.40522266 x4 - x15 <= 0 e40: - 1.69606209 x6 + 0.19678752 x7 - x16 <= 0 e41: 1.52787272 x9 + 3.47213745 x10 - x17 <= 0 e42: 1.04912586 x12 - 3.14748592 x13 - x18 <= 0 e43: 1.52787272 x9 - 1.52786255 x10 - x17 <= 0 e44: - 2.24629156 x3 + 0.20410502 x4 - x15 >= -10 e45: 1.42893791 x6 + 3.94678752 x7 - x16 >= -10 e46: - 2.47212728 x9 - 1.52786255 x10 - x17 >= -10 e47: - 1.63415571 x12 + 0.43022284 x13 - x18 >= -10 e48: 1.59481484 x3 + 3.40502701 x4 - x15 >= -10 e49: 1.42893791 x6 - 6.05321248 x7 - x16 >= -10 e50: - 0.47212728 x9 + 2.47213745 x10 - x17 >= -10 e51: 1.04912586 x12 + 1.60415853 x13 - x18 >= -10 e52: 1.59481484 x3 - 4.40522266 x4 - x15 >= -10 e53: - 1.69606209 x6 + 0.19678752 x7 - x16 >= -10 e54: 1.52787272 x9 + 3.47213745 x10 - x17 >= -10 e55: 1.04912586 x12 - 3.14748592 x13 - x18 >= -10 e56: 1.52787272 x9 - 1.52786255 x10 - x17 >= -10 e57: [ x3^2 + x4^2 ] = 1 e58: [ x6^2 + x7^2 ] = 1 e59: [ x9^2 + x10^2 ] = 1 e60: [ x12^2 + x13^2 ] = 1 e61: [ x5^2 - 2 x5 * x8 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 9.143040659 e62: [ x5^2 - 2 x5 * x11 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 9.751079108 e63: [ x5^2 - 2 x5 * x14 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 6.990422425 e64: [ x5^2 - 4.5236206 x5 * x6 - 1.06782914 x5 * x7 - 2 x5 * x8 + 5.400850601 x6^2 + 4.5236206 x6 * x8 + 1.06782914 x6 * x15 - 1.06782914 x6 * x16 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 4.5236206 x7 * x15 + 4.5236206 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 6.199294212 e65: [ x5^2 + 4.3914795 x5 * x9 - 1.47802734 x5 * x10 - 2 x5 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x15 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x15 - 4.3914795 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 5.681888199 e66: [ x5^2 - 3.02492942 x5 * x12 - 1.00827778 x5 * x13 - 2 x5 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x15 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x15 + 3.02492942 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 4.578751829 e67: [ x5^2 + 4.009552 x5 * x6 - 1.45166714 x5 * x7 - 2 x5 * x8 + 4.545961182 x6^2 - 4.009552 x6 * x8 + 1.45166714 x6 * x15 - 1.45166714 x6 * x16 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 4.009552 x7 * x15 - 4.009552 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 5.280432558 e68: [ x5^2 - 2.10591634 x5 * x9 + 3.40738932 x5 * x10 - 2 x5 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x15 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x15 + 2.10591634 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 4.28373765 e69: [ x5^2 + 2.26962754 x5 * x12 - 1.48442486 x5 * x13 - 2 x5 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x15 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x15 - 2.26962754 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 3.616570413 e70: [ x5^2 - 7.357076 x5 * x6 - 1.7367363 x5 * x7 - 2 x5 * x8 + 14.28570506 x6^2 + 7.357076 x6 * x8 + 1.7367363 x6 * x15 - 1.7367363 x6 * x16 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 7.357076 x7 * x15 + 7.357076 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 4.645682774 e71: [ x5^2 + 2.9976666 x5 * x9 - 0.70766974 x5 * x10 - 2 x5 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x15 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x15 - 2.9976666 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 7.666545219 e72: [ x5^2 - 4.59619514 x5 * x12 - 1.53205596 x5 * x13 - 2 x5 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x15 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x15 + 4.59619514 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 3.526556221 e73: [ x5^2 - 9.1317749 x5 * x6 - 2.15565364 x5 * x7 - 2 x5 * x8 + 22.00903886 x6^2 + 9.1317749 x6 * x8 + 2.15565364 x6 * x15 - 2.15565364 x6 * x16 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 9.1317749 x7 * x15 + 9.1317749 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 3.786618307 e74: [ x5^2 - 2.5314331 x5 * x9 - 2.53149414 x5 * x10 - 2 x5 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x15 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x15 + 2.5314331 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 3.448227983 e75: [ x5^2 + 0.65916112 x5 * x12 + 2.50375742 x5 * x13 - 2 x5 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x15 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x15 - 0.65916112 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 3.386493673 e76: [ x8^2 - 2 x8 * x11 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 8.742596696 e77: [ x8^2 - 2 x8 * x14 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 6.140767239 e78: [ x8^2 + 4.3914795 x8 * x9 - 1.47802734 x8 * x10 - 2 x8 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x16 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x16 - 4.3914795 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 4.918581883 e79: [ x8^2 - 3.02492942 x8 * x12 - 1.00827778 x8 * x13 - 2 x8 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x16 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x16 + 3.02492942 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 3.896353337 e80: [ x8^2 - 2.10591634 x8 * x9 + 3.40738932 x8 * x10 - 2 x8 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x16 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x16 + 2.10591634 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 3.624590258 e81: [ x8^2 + 2.26962754 x8 * x12 - 1.48442486 x8 * x13 - 2 x8 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x16 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x16 - 2.26962754 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 3.013156892 e82: [ x8^2 + 2.9976666 x8 * x9 - 0.70766974 x8 * x10 - 2 x8 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x16 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x16 - 2.9976666 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 6.775448344 e83: [ x8^2 - 4.59619514 x8 * x12 - 1.53205596 x8 * x13 - 2 x8 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x16 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x16 + 4.59619514 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 2.931043913 e84: [ x8^2 - 2.5314331 x8 * x9 - 2.53149414 x8 * x10 - 2 x8 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x16 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x16 + 2.5314331 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 2.859673574 e85: [ x8^2 + 0.65916112 x8 * x12 + 2.50375742 x8 * x13 - 2 x8 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x16 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x16 - 0.65916112 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 2.803478999 e86: [ x11^2 - 2 x11 * x14 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 6.640840403 e87: [ x11^2 - 3.02492942 x11 * x12 - 1.00827778 x11 * x13 - 2 x11 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x17 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x17 + 3.02492942 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 4.296681958 e88: [ x11^2 + 2.26962754 x11 * x12 - 1.48442486 x11 * x13 - 2 x11 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x17 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x17 - 2.26962754 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 3.366382347 e89: [ x11^2 - 4.59619514 x11 * x12 - 1.53205596 x11 * x13 - 2 x11 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x17 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x17 + 4.59619514 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 3.279557433 e90: [ x11^2 + 0.65916112 x11 * x12 + 2.50375742 x11 * x13 - 2 x11 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x17 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x17 - 0.65916112 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 3.144539478 e91: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 4.47509892 x3 * x8 - 1.61999788 x3 * x15 + 1.61999788 x3 * x16 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 1.61999788 x4 * x8 + 4.47509892 x4 * x15 - 4.47509892 x4 * x16 + x5^2 - 2 x5 * x8 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 4.900598653 e92: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 4.47509892 x3 * x11 - 1.61999788 x3 * x15 + 1.61999788 x3 * x17 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 1.61999788 x4 * x11 + 4.47509892 x4 * x15 - 4.47509892 x4 * x17 + x5^2 - 2 x5 * x11 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 5.348374259 e93: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 4.47509892 x3 * x14 - 1.61999788 x3 * x15 + 1.61999788 x3 * x18 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 1.61999788 x4 * x14 + 4.47509892 x4 * x15 - 4.47509892 x4 * x18 + x5^2 - 2 x5 * x14 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 3.363277788 e94: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 10.9867653 x3 * x6 + 1.274807375 x3 * x7 - 4.47509892 x3 * x8 - 1.61999788 x3 * x15 + 1.61999788 x3 * x16 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 1.274807375 x4 * x6 - 10.9867653 x4 * x7 - 1.61999788 x4 * x8 + 4.47509892 x4 * x15 - 4.47509892 x4 * x16 + x5^2 - 4.5236206 x5 * x6 - 1.06782914 x5 * x7 - 2 x5 * x8 + 5.400850601 x6^2 + 4.5236206 x6 * x8 + 1.06782914 x6 * x15 - 1.06782914 x6 * x16 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 4.5236206 x7 * x15 + 4.5236206 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 2.821800742 e95: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 + 8.628952005 x3 * x9 - 6.864253017 x3 * x10 - 4.47509892 x3 * x11 - 1.61999788 x3 * x15 + 1.61999788 x3 * x17 + 5.662725869 x4^2 + 1.61999788 x4 * x5 + 6.864253017 x4 * x9 + 8.628952005 x4 * x10 - 1.61999788 x4 * x11 + 4.47509892 x4 * x15 - 4.47509892 x4 * x17 + x5^2 + 4.3914795 x5 * x9 - 1.47802734 x5 * x10 - 2 x5 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x15 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x15 - 4.3914795 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 2.476388832 e96: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 7.585133123 x3 * x12 + 0.1941182216 x3 * x13 - 4.47509892 x3 * x14 - 1.61999788 x3 * x15 + 1.61999788 x3 * x18 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 0.1941182216 x4 * x12 - 7.585133123 x4 * x13 - 1.61999788 x4 * x14 + 4.47509892 x4 * x15 - 4.47509892 x4 * x18 + x5^2 - 3.02492942 x5 * x12 - 1.00827778 x5 * x13 - 2 x5 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x15 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x15 + 3.02492942 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 1.768328864 e97: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 + 7.795722068 x3 * x6 - 6.495909895 x3 * x7 - 4.47509892 x3 * x8 - 1.61999788 x3 * x15 + 1.61999788 x3 * x16 + 5.662725869 x4^2 + 1.61999788 x4 * x5 + 6.495909895 x4 * x6 + 7.795722068 x4 * x7 - 1.61999788 x4 * x8 + 4.47509892 x4 * x15 - 4.47509892 x4 * x16 + x5^2 + 4.009552 x5 * x6 - 1.45166714 x5 * x7 - 2 x5 * x8 + 4.545961182 x6^2 - 4.009552 x6 * x8 + 1.45166714 x6 * x15 - 1.45166714 x6 * x16 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 4.009552 x7 * x15 - 4.009552 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 2.213854236 e98: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 1.952110232 x3 * x9 + 9.329992136 x3 * x10 - 4.47509892 x3 * x11 - 1.61999788 x3 * x15 + 1.61999788 x3 * x17 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 9.329992136 x4 * x9 - 1.952110232 x4 * x10 - 1.61999788 x4 * x11 + 4.47509892 x4 * x15 - 4.47509892 x4 * x17 + x5^2 - 2.10591634 x5 * x9 + 3.40738932 x5 * x10 - 2 x5 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x15 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x15 + 2.10591634 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 1.586850817 e99: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 + 3.876021313 x3 * x12 - 5.159869945 x3 * x13 - 4.47509892 x3 * x14 - 1.61999788 x3 * x15 + 1.61999788 x3 * x18 + 5.662725869 x4^2 + 1.61999788 x4 * x5 + 5.159869945 x4 * x12 + 3.876021313 x4 * x13 - 1.61999788 x4 * x14 + 4.47509892 x4 * x15 - 4.47509892 x4 * x18 + x5^2 + 2.26962754 x5 * x12 - 1.48442486 x5 * x13 - 2 x5 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x15 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x15 - 2.26962754 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 1.19183448 e100: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 17.86857599 x3 * x6 + 2.073190391 x3 * x7 - 4.47509892 x3 * x8 - 1.61999788 x3 * x15 + 1.61999788 x3 * x16 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 2.073190391 x4 * x6 - 17.86857599 x4 * x7 - 1.61999788 x4 * x8 + 4.47509892 x4 * x15 - 4.47509892 x4 * x16 + x5^2 - 7.357076 x5 * x6 - 1.7367363 x5 * x7 - 2 x5 * x8 + 14.28570506 x6^2 + 7.357076 x6 * x8 + 1.7367363 x6 * x15 - 1.7367363 x6 * x16 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 7.357076 x7 * x15 + 7.357076 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.81001519 e101: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 + 6.134215543 x3 * x9 - 4.011552813 x3 * x10 - 4.47509892 x3 * x11 - 1.61999788 x3 * x15 + 1.61999788 x3 * x17 + 5.662725869 x4^2 + 1.61999788 x4 * x5 + 4.011552813 x4 * x9 + 6.134215543 x4 * x10 - 1.61999788 x4 * x11 + 4.47509892 x4 * x15 - 4.47509892 x4 * x17 + x5^2 + 2.9976666 x5 * x9 - 0.70766974 x5 * x10 - 2 x5 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x15 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x15 - 2.9976666 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 3.837039023 e102: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 11.52517766 x3 * x12 + 0.2948622054 x3 * x13 - 4.47509892 x3 * x14 - 1.61999788 x3 * x15 + 1.61999788 x3 * x18 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 0.2948622054 x4 * x12 - 11.52517766 x4 * x13 - 1.61999788 x4 * x14 + 4.47509892 x4 * x15 - 4.47509892 x4 * x18 + x5^2 - 4.59619514 x5 * x12 - 1.53205596 x5 * x13 - 2 x5 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x15 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x15 + 4.59619514 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 1.140402251 e103: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 22.17887516 x3 * x6 + 2.573346351 x3 * x7 - 4.47509892 x3 * x8 - 1.61999788 x3 * x15 + 1.61999788 x3 * x16 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 2.573346351 x4 * x6 - 22.17887516 x4 * x7 - 1.61999788 x4 * x8 + 4.47509892 x4 * x15 - 4.47509892 x4 * x16 + x5^2 - 9.1317749 x5 * x6 - 2.15565364 x5 * x7 - 2 x5 * x8 + 22.00903886 x6^2 + 9.1317749 x6 * x8 + 2.15565364 x6 * x15 - 2.15565364 x6 * x16 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 9.1317749 x7 * x15 + 9.1317749 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.290284622 e104: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 - 7.714714336 x3 * x9 - 3.613885218 x3 * x10 - 4.47509892 x3 * x11 - 1.61999788 x3 * x15 + 1.61999788 x3 * x17 + 5.662725869 x4^2 + 1.61999788 x4 * x5 + 3.613885218 x4 * x9 - 7.714714336 x4 * x10 - 1.61999788 x4 * x11 + 4.47509892 x4 * x15 - 4.47509892 x4 * x17 + x5^2 - 2.5314331 x5 * x9 - 2.53149414 x5 * x10 - 2 x5 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x15 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x15 + 2.5314331 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 1.096049736 e105: [ 5.662725869 x3^2 + 4.47509892 x3 * x5 + 3.502946464 x3 * x12 + 5.068361255 x3 * x13 - 4.47509892 x3 * x14 - 1.61999788 x3 * x15 + 1.61999788 x3 * x18 + 5.662725869 x4^2 + 1.61999788 x4 * x5 - 5.068361255 x4 * x12 + 3.502946464 x4 * x13 - 1.61999788 x4 * x14 + 4.47509892 x4 * x15 - 4.47509892 x4 * x18 + x5^2 + 0.65916112 x5 * x12 + 2.50375742 x5 * x13 - 2 x5 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x15 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x15 - 0.65916112 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 1.061366188 e106: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 - 4.5236206 x6 * x11 - 1.06782914 x6 * x16 + 1.06782914 x6 * x17 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 1.06782914 x7 * x11 + 4.5236206 x7 * x16 - 4.5236206 x7 * x17 + x8^2 - 2 x8 * x11 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 5.870348948 e107: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 - 4.5236206 x6 * x14 - 1.06782914 x6 * x16 + 1.06782914 x6 * x18 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 1.06782914 x7 * x14 + 4.5236206 x7 * x16 - 4.5236206 x7 * x18 + x8^2 - 2 x8 * x14 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 3.779716151 e108: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 + 9.143553234 x6 * x9 - 5.68769235 x6 * x10 - 4.5236206 x6 * x11 - 1.06782914 x6 * x16 + 1.06782914 x6 * x17 + 5.400850601 x7^2 + 1.06782914 x7 * x8 + 5.68769235 x7 * x9 + 9.143553234 x7 * x10 - 1.06782914 x7 * x11 + 4.5236206 x7 * x16 - 4.5236206 x7 * x17 + x8^2 + 4.3914795 x8 * x9 - 1.47802734 x8 * x10 - 2 x8 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x16 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x16 - 4.3914795 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 2.835450743 e109: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 - 7.380150716 x6 * x12 - 0.6654791775 x6 * x13 - 4.5236206 x6 * x14 - 1.06782914 x6 * x16 + 1.06782914 x6 * x18 + 5.400850601 x7^2 + 1.06782914 x7 * x8 + 0.6654791775 x7 * x12 - 7.380150716 x7 * x13 - 1.06782914 x7 * x14 + 4.5236206 x7 * x16 - 4.5236206 x7 * x18 + x8^2 - 3.02492942 x8 * x12 - 1.00827778 x8 * x13 - 2 x8 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x16 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x16 + 3.02492942 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 2.073629751 e110: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 - 2.943928465 x6 * x9 + 8.831247677 x6 * x10 - 4.5236206 x6 * x11 - 1.06782914 x6 * x16 + 1.06782914 x6 * x17 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 8.831247677 x7 * x9 - 2.943928465 x7 * x10 - 1.06782914 x7 * x11 + 4.5236206 x7 * x16 - 4.5236206 x7 * x17 + x8^2 - 2.10591634 x8 * x9 + 3.40738932 x8 * x10 - 2 x8 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x16 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x16 + 2.10591634 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 1.876701985 e111: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 + 4.340910886 x6 * x12 - 4.56927465 x6 * x13 - 4.5236206 x6 * x14 - 1.06782914 x6 * x16 + 1.06782914 x6 * x18 + 5.400850601 x7^2 + 1.06782914 x7 * x8 + 4.56927465 x7 * x12 + 4.340910886 x7 * x13 - 1.06782914 x7 * x14 + 4.5236206 x7 * x16 - 4.5236206 x7 * x18 + x8^2 + 2.26962754 x8 * x12 - 1.48442486 x8 * x13 - 2 x8 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x16 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x16 - 2.26962754 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.444652023 e112: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 + 6.402318007 x6 * x9 - 3.201112581 x6 * x10 - 4.5236206 x6 * x11 - 1.06782914 x6 * x16 + 1.06782914 x6 * x17 + 5.400850601 x7^2 + 1.06782914 x7 * x8 + 3.201112581 x7 * x9 + 6.402318007 x7 * x10 - 1.06782914 x7 * x11 + 4.5236206 x7 * x16 - 4.5236206 x7 * x17 + x8^2 + 2.9976666 x8 * x9 - 0.70766974 x8 * x10 - 2 x8 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x16 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x16 - 2.9976666 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 4.281014249 e113: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 - 11.21370851 x6 * x12 - 1.011244399 x6 * x13 - 4.5236206 x6 * x14 - 1.06782914 x6 * x16 + 1.06782914 x6 * x18 + 5.400850601 x7^2 + 1.06782914 x7 * x8 + 1.011244399 x7 * x12 - 11.21370851 x7 * x13 - 1.06782914 x7 * x14 + 4.5236206 x7 * x16 - 4.5236206 x7 * x18 + x8^2 - 4.59619514 x8 * x12 - 1.53205596 x8 * x13 - 2 x8 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x16 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x16 + 4.59619514 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.387969656 e114: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 - 7.077223065 x6 * x9 - 4.374190505 x6 * x10 - 4.5236206 x6 * x11 - 1.06782914 x6 * x16 + 1.06782914 x6 * x17 + 5.400850601 x7^2 + 1.06782914 x7 * x8 + 4.374190505 x7 * x9 - 7.077223065 x7 * x10 - 1.06782914 x7 * x11 + 4.5236206 x7 * x16 - 4.5236206 x7 * x17 + x8^2 - 2.5314331 x8 * x9 - 2.53149414 x8 * x10 - 2 x8 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x16 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x16 + 2.5314331 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 1.338993808 e115: [ 5.400850601 x6^2 + 4.5236206 x6 * x8 + 2.827689977 x6 * x12 + 5.311088595 x6 * x13 - 4.5236206 x6 * x14 - 1.06782914 x6 * x16 + 1.06782914 x6 * x18 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 5.311088595 x7 * x12 + 2.827689977 x7 * x13 - 1.06782914 x7 * x14 + 4.5236206 x7 * x16 - 4.5236206 x7 * x18 + x8^2 + 0.65916112 x8 * x12 + 2.50375742 x8 * x13 - 2 x8 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x16 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x16 - 0.65916112 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.300629259 e116: [ 5.367414254 x9^2 - 4.3914795 x9 * x11 + 4.3914795 x9 * x14 - 1.47802734 x9 * x17 + 1.47802734 x9 * x18 + 5.367414254 x10^2 + 1.47802734 x10 * x11 - 1.47802734 x10 * x14 - 4.3914795 x10 * x17 + 4.3914795 x10 * x18 + x11^2 - 2 x11 * x14 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 3.378178494 e117: [ 5.367414254 x9^2 - 4.3914795 x9 * x11 + 5.896826706 x9 * x12 + 4.449379793 x9 * x13 + 4.3914795 x9 * x14 - 1.47802734 x9 * x17 + 1.47802734 x9 * x18 + 5.367414254 x10^2 + 1.47802734 x10 * x11 - 4.449379793 x10 * x12 + 5.896826706 x10 * x13 - 1.47802734 x10 * x14 - 4.3914795 x10 * x17 + 4.3914795 x10 * x18 + x11^2 - 3.02492942 x11 * x12 - 1.00827778 x11 * x13 - 2 x11 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x17 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x17 + 3.02492942 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 1.779137949 e118: [ 5.367414254 x9^2 - 4.3914795 x9 * x11 - 6.080521671 x9 * x12 + 1.582124893 x9 * x13 + 4.3914795 x9 * x14 - 1.47802734 x9 * x17 + 1.47802734 x9 * x18 + 5.367414254 x10^2 + 1.47802734 x10 * x11 - 1.582124893 x10 * x12 - 6.080521671 x10 * x13 - 1.47802734 x10 * x14 - 4.3914795 x10 * x17 + 4.3914795 x10 * x18 + x11^2 + 2.26962754 x11 * x12 - 1.48442486 x11 * x13 - 2 x11 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x17 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x17 - 2.26962754 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 1.200711345 e119: [ 5.367414254 x9^2 - 4.3914795 x9 * x11 + 8.95983807 x9 * x12 + 6.760647209 x9 * x13 + 4.3914795 x9 * x14 - 1.47802734 x9 * x17 + 1.47802734 x9 * x18 + 5.367414254 x10^2 + 1.47802734 x10 * x11 - 6.760647209 x10 * x12 + 8.95983807 x10 * x13 - 1.47802734 x10 * x14 - 4.3914795 x10 * x17 + 4.3914795 x10 * x18 + x11^2 - 4.59619514 x11 * x12 - 1.53205596 x11 * x13 - 2 x11 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x17 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x17 + 4.59619514 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 1.149085828 e120: [ 5.367414254 x9^2 - 4.3914795 x9 * x11 + 0.4029646869 x9 * x12 - 5.98472877 x9 * x13 + 4.3914795 x9 * x14 - 1.47802734 x9 * x17 + 1.47802734 x9 * x18 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 5.98472877 x10 * x12 + 0.4029646869 x10 * x13 - 1.47802734 x10 * x14 - 4.3914795 x10 * x17 + 4.3914795 x10 * x18 + x11^2 + 0.65916112 x11 * x12 + 2.50375742 x11 * x13 - 2 x11 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x17 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x17 - 0.65916112 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 1.069744034 e121: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 4.05647702 x3 * x8 - 1.89996134 x3 * x15 + 1.89996134 x3 * x16 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 1.89996134 x4 * x8 - 4.05647702 x4 * x15 + 4.05647702 x4 * x16 + x5^2 - 2 x5 * x8 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 4.300503225 e122: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 4.05647702 x3 * x11 - 1.89996134 x3 * x15 + 1.89996134 x3 * x17 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 1.89996134 x4 * x11 - 4.05647702 x4 * x15 + 4.05647702 x4 * x17 + x5^2 - 2 x5 * x11 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 4.720586746 e123: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 4.05647702 x3 * x14 - 1.89996134 x3 * x15 + 1.89996134 x3 * x18 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 1.89996134 x4 * x14 - 4.05647702 x4 * x15 + 4.05647702 x4 * x18 + x5^2 - 2 x5 * x14 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 2.869500617 e124: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 8.160564464 x3 * x6 + 6.463164312 x3 * x7 + 4.05647702 x3 * x8 - 1.89996134 x3 * x15 + 1.89996134 x3 * x16 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 6.463164312 x4 * x6 + 8.160564464 x4 * x7 - 1.89996134 x4 * x8 - 4.05647702 x4 * x15 + 4.05647702 x4 * x16 + x5^2 - 4.5236206 x5 * x6 - 1.06782914 x5 * x7 - 2 x5 * x8 + 5.400850601 x6^2 + 4.5236206 x6 * x8 + 1.06782914 x6 * x15 - 1.06782914 x6 * x16 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 4.5236206 x7 * x15 + 4.5236206 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 2.371161213 e125: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 - 10.31106524 x3 * x9 - 1.174028668 x3 * x10 + 4.05647702 x3 * x11 - 1.89996134 x3 * x15 + 1.89996134 x3 * x17 + 5.016214727 x4^2 + 1.89996134 x4 * x5 + 1.174028668 x4 * x9 - 10.31106524 x4 * x10 - 1.89996134 x4 * x11 - 4.05647702 x4 * x15 + 4.05647702 x4 * x17 + x5^2 + 4.3914795 x5 * x9 - 1.47802734 x5 * x10 - 2 x5 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x15 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x15 - 4.3914795 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 2.05546845 e126: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 5.177433939 x3 * x12 + 4.918652299 x3 * x13 + 4.05647702 x3 * x14 - 1.89996134 x3 * x15 + 1.89996134 x3 * x18 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 4.918652299 x4 * x12 + 5.177433939 x4 * x13 - 1.89996134 x4 * x14 - 4.05647702 x4 * x15 + 4.05647702 x4 * x18 + x5^2 - 3.02492942 x5 * x12 - 1.00827778 x5 * x13 - 2 x5 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x15 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x15 + 3.02492942 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 1.415674393 e127: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 - 9.511383497 x3 * x6 - 0.8646696983 x3 * x7 + 4.05647702 x3 * x8 - 1.89996134 x3 * x15 + 1.89996134 x3 * x16 + 5.016214727 x4^2 + 1.89996134 x4 * x5 + 0.8646696983 x4 * x6 - 9.511383497 x4 * x7 - 1.89996134 x4 * x8 - 4.05647702 x4 * x15 + 4.05647702 x4 * x16 + x5^2 + 4.009552 x5 * x6 - 1.45166714 x5 * x7 - 2 x5 * x8 + 4.545961182 x6^2 - 4.009552 x6 * x8 + 1.45166714 x6 * x15 - 1.45166714 x6 * x16 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 4.009552 x7 * x15 - 4.009552 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.816938254 e128: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 7.508254609 x3 * x9 - 4.910418422 x3 * x10 + 4.05647702 x3 * x11 - 1.89996134 x3 * x15 + 1.89996134 x3 * x17 + 5.016214727 x4^2 + 1.89996134 x4 * x5 + 4.910418422 x4 * x9 + 7.508254609 x4 * x10 - 1.89996134 x4 * x11 - 4.05647702 x4 * x15 + 4.05647702 x4 * x17 + x5^2 - 2.10591634 x5 * x9 + 3.40738932 x5 * x10 - 2 x5 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x15 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x15 + 2.10591634 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 1.253814443 e129: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 - 6.013520903 x3 * x12 + 0.8546653752 x3 * x13 + 4.05647702 x3 * x14 - 1.89996134 x3 * x15 + 1.89996134 x3 * x18 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 0.8546653752 x4 * x12 - 6.013520903 x4 * x13 - 1.89996134 x4 * x14 - 4.05647702 x4 * x15 + 4.05647702 x4 * x18 + x5^2 + 2.26962754 x5 * x12 - 1.48442486 x5 * x13 - 2 x5 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x15 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x15 - 2.26962754 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.9058235131 e130: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 13.27203895 x3 * x6 + 10.51159543 x3 * x7 + 4.05647702 x3 * x8 - 1.89996134 x3 * x15 + 1.89996134 x3 * x16 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 10.51159543 x4 * x6 + 13.27203895 x4 * x7 - 1.89996134 x4 * x8 - 4.05647702 x4 * x15 + 4.05647702 x4 * x16 + x5^2 - 7.357076 x5 * x6 - 1.7367363 x5 * x7 - 2 x5 * x8 + 14.28570506 x6^2 + 7.357076 x6 * x8 + 1.7367363 x6 * x15 - 1.7367363 x6 * x16 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 7.357076 x7 * x15 + 7.357076 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.452998659 e131: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 - 6.752255412 x3 * x9 - 1.412402306 x3 * x10 + 4.05647702 x3 * x11 - 1.89996134 x3 * x15 + 1.89996134 x3 * x17 + 5.016214727 x4^2 + 1.89996134 x4 * x5 + 1.412402306 x4 * x9 - 6.752255412 x4 * x10 - 1.89996134 x4 * x11 - 4.05647702 x4 * x15 + 4.05647702 x4 * x17 + x5^2 + 2.9976666 x5 * x9 - 0.70766974 x5 * x10 - 2 x5 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x15 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x15 - 2.9976666 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 3.308295462 e132: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 7.866756435 x3 * x12 + 7.473671436 x3 * x13 + 4.05647702 x3 * x14 - 1.89996134 x3 * x15 + 1.89996134 x3 * x18 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 7.473671436 x4 * x12 + 7.866756435 x4 * x13 - 1.89996134 x4 * x14 - 4.05647702 x4 * x15 + 4.05647702 x4 * x18 + x5^2 - 4.59619514 x5 * x12 - 1.53205596 x5 * x13 - 2 x5 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x15 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x15 + 4.59619514 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.8610579265 e133: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 16.47358823 x3 * x6 + 13.04718936 x3 * x7 + 4.05647702 x3 * x8 - 1.89996134 x3 * x15 + 1.89996134 x3 * x16 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 13.04718936 x4 * x6 + 16.47358823 x4 * x7 - 1.89996134 x4 * x8 - 4.05647702 x4 * x15 + 4.05647702 x4 * x16 + x5^2 - 9.1317749 x5 * x6 - 2.15565364 x5 * x7 - 2 x5 * x8 + 22.00903886 x6^2 + 9.1317749 x6 * x8 + 2.15565364 x6 * x15 - 2.15565364 x6 * x16 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 9.1317749 x7 * x15 + 9.1317749 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 0.9919021605 e134: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 2.7294796 x3 * x9 + 7.539286415 x3 * x10 + 4.05647702 x3 * x11 - 1.89996134 x3 * x15 + 1.89996134 x3 * x17 + 5.016214727 x4^2 + 1.89996134 x4 * x5 - 7.539286415 x4 * x9 + 2.7294796 x4 * x10 - 1.89996134 x4 * x11 - 4.05647702 x4 * x15 + 4.05647702 x4 * x17 + x5^2 - 2.5314331 x5 * x9 - 2.53149414 x5 * x10 - 2 x5 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x15 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x15 + 2.5314331 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 0.8225761332 e135: [ 5.016214727 x3^2 - 4.05647702 x3 * x5 + 1.041585183 x3 * x12 - 5.704407541 x3 * x13 + 4.05647702 x3 * x14 - 1.89996134 x3 * x15 + 1.89996134 x3 * x18 + 5.016214727 x4^2 + 1.89996134 x4 * x5 + 5.704407541 x4 * x12 + 1.041585183 x4 * x13 - 1.89996134 x4 * x14 - 4.05647702 x4 * x15 + 4.05647702 x4 * x18 + x5^2 + 0.65916112 x5 * x12 + 2.50375742 x5 * x13 - 2 x5 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x15 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x15 - 0.65916112 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.7925667313 e136: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 4.009552 x6 * x11 - 1.45166714 x6 * x16 + 1.45166714 x6 * x17 + 4.545961182 x7^2 + 1.45166714 x7 * x8 - 1.45166714 x7 * x11 - 4.009552 x7 * x16 + 4.009552 x7 * x17 + x8^2 - 2 x8 * x11 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 4.977188277 e137: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 4.009552 x6 * x14 - 1.45166714 x6 * x16 + 1.45166714 x6 * x18 + 4.545961182 x7^2 + 1.45166714 x7 * x8 - 1.45166714 x7 * x14 - 4.009552 x7 * x16 + 4.009552 x7 * x18 + x8^2 - 2 x8 * x14 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 3.070310674 e138: [ 4.545961182 x6^2 - 4.009552 x6 * x8 - 9.876734567 x6 * x9 - 0.2243695045 x6 * x10 + 4.009552 x6 * x11 - 1.45166714 x6 * x16 + 1.45166714 x6 * x17 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 0.2243695045 x7 * x9 - 9.876734567 x7 * x10 - 1.45166714 x7 * x11 - 4.009552 x7 * x16 + 4.009552 x7 * x17 + x8^2 + 4.3914795 x8 * x9 - 1.47802734 x8 * x10 - 2 x8 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x16 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x16 - 4.3914795 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 2.225946611 e139: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 5.332464042 x6 * x12 + 4.216966415 x6 * x13 + 4.009552 x6 * x14 - 1.45166714 x6 * x16 + 1.45166714 x6 * x18 + 4.545961182 x7^2 + 1.45166714 x7 * x8 - 4.216966415 x7 * x12 + 5.332464042 x7 * x13 - 1.45166714 x7 * x14 - 4.009552 x7 * x16 + 4.009552 x7 * x18 + x8^2 - 3.02492942 x8 * x12 - 1.00827778 x8 * x13 - 2 x8 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x16 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x16 + 3.02492942 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.557731943 e140: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 6.695088091 x6 * x9 - 5.302507556 x6 * x10 + 4.009552 x6 * x11 - 1.45166714 x6 * x16 + 1.45166714 x6 * x17 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 5.302507556 x7 * x9 + 6.695088091 x7 * x10 - 1.45166714 x7 * x11 - 4.009552 x7 * x16 + 4.009552 x7 * x17 + x8^2 - 2.10591634 x8 * x9 + 3.40738932 x8 * x10 - 2 x8 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x16 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x16 + 2.10591634 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 1.387704544 e141: [ 4.545961182 x6^2 - 4.009552 x6 * x8 - 5.627540217 x6 * x12 + 1.328567473 x6 * x13 + 4.009552 x6 * x14 - 1.45166714 x6 * x16 + 1.45166714 x6 * x18 + 4.545961182 x7^2 + 1.45166714 x7 * x8 - 1.328567473 x7 * x12 - 5.627540217 x7 * x13 - 1.45166714 x7 * x14 - 4.009552 x7 * x16 + 4.009552 x7 * x18 + x8^2 + 2.26962754 x8 * x12 - 1.48442486 x8 * x13 - 2 x8 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x16 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x16 - 2.26962754 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.020135896 e142: [ 4.545961182 x6^2 - 4.009552 x6 * x8 - 6.523300509 x6 * x9 - 0.7570877393 x6 * x10 + 4.009552 x6 * x11 - 1.45166714 x6 * x16 + 1.45166714 x6 * x17 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 0.7570877393 x7 * x9 - 6.523300509 x7 * x10 - 1.45166714 x7 * x11 - 4.009552 x7 * x16 + 4.009552 x7 * x17 + x8^2 + 2.9976666 x8 * x9 - 0.70766974 x8 * x10 - 2 x8 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x16 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x16 - 2.9976666 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 3.523662801 e143: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 8.102324061 x6 * x12 + 6.407501746 x6 * x13 + 4.009552 x6 * x14 - 1.45166714 x6 * x16 + 1.45166714 x6 * x18 + 4.545961182 x7^2 + 1.45166714 x7 * x8 - 6.407501746 x7 * x12 + 8.102324061 x7 * x13 - 1.45166714 x7 * x14 - 4.009552 x7 * x16 + 4.009552 x7 * x18 + x8^2 - 4.59619514 x8 * x12 - 1.53205596 x8 * x13 - 2 x8 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x16 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x16 + 4.59619514 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.9725948385 e144: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 3.237512895 x6 * x9 + 6.91247782 x6 * x10 + 4.009552 x6 * x11 - 1.45166714 x6 * x16 + 1.45166714 x6 * x17 + 4.545961182 x7^2 + 1.45166714 x7 * x8 - 6.91247782 x7 * x9 + 3.237512895 x7 * x10 - 1.45166714 x7 * x11 - 4.009552 x7 * x16 + 4.009552 x7 * x17 + x8^2 - 2.5314331 x8 * x9 - 2.53149414 x8 * x10 - 2 x8 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x16 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x16 + 2.5314331 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 0.9316689336 e145: [ 4.545961182 x6^2 - 4.009552 x6 * x8 + 0.4958407931 x6 * x12 - 5.497914054 x6 * x13 + 4.009552 x6 * x14 - 1.45166714 x6 * x16 + 1.45166714 x6 * x18 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 5.497914054 x7 * x12 + 0.4958407931 x7 * x13 - 1.45166714 x7 * x14 - 4.009552 x7 * x16 + 4.009552 x7 * x18 + x8^2 + 0.65916112 x8 * x12 + 2.50375742 x8 * x13 - 2 x8 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x16 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x16 - 0.65916112 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.8997135811 e146: [ 4.011296402 x9^2 + 2.10591634 x9 * x11 - 2.10591634 x9 * x14 + 3.40738932 x9 * x17 - 3.40738932 x9 * x18 + 4.011296402 x10^2 - 3.40738932 x10 * x11 + 3.40738932 x10 * x14 + 2.10591634 x10 * x17 - 2.10591634 x10 * x18 + x11^2 - 2 x11 * x14 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 2.322668172 e147: [ 4.011296402 x9^2 + 2.10591634 x9 * x11 - 1.467326677 x9 * x12 - 6.215230426 x9 * x13 - 2.10591634 x9 * x14 + 3.40738932 x9 * x17 - 3.40738932 x9 * x18 + 4.011296402 x10^2 - 3.40738932 x10 * x11 + 6.215230426 x10 * x12 - 1.467326677 x10 * x13 + 3.40738932 x10 * x14 + 2.10591634 x10 * x17 - 2.10591634 x10 * x18 + x11^2 - 3.02492942 x11 * x12 - 1.00827778 x11 * x13 - 2 x11 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x17 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x17 + 3.02492942 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 1.040178386 e148: [ 4.011296402 x9^2 + 2.10591634 x9 * x11 + 4.918829568 x9 * x12 + 2.303715036 x9 * x13 - 2.10591634 x9 * x14 + 3.40738932 x9 * x17 - 3.40738932 x9 * x18 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.303715036 x10 * x12 + 4.918829568 x10 * x13 + 3.40738932 x10 * x14 + 2.10591634 x10 * x17 - 2.10591634 x10 * x18 + x11^2 + 2.26962754 x11 * x12 - 1.48442486 x11 * x13 - 2 x11 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x17 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x17 - 2.26962754 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.611239088 e149: [ 4.011296402 x9^2 + 2.10591634 x9 * x11 - 2.229445666 x9 * x12 - 9.443703956 x9 * x13 - 2.10591634 x9 * x14 + 3.40738932 x9 * x17 - 3.40738932 x9 * x18 + 4.011296402 x10^2 - 3.40738932 x10 * x11 + 9.443703956 x10 * x12 - 2.229445666 x10 * x13 + 3.40738932 x10 * x14 + 2.10591634 x10 * x17 - 2.10591634 x10 * x18 + x11^2 - 4.59619514 x11 * x12 - 1.53205596 x11 * x13 - 2 x11 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x17 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x17 + 4.59619514 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.5745674413 e150: [ 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.57156906 x9 * x12 + 3.759361111 x9 * x13 - 2.10591634 x9 * x14 + 3.40738932 x9 * x17 - 3.40738932 x9 * x18 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 3.759361111 x10 * x12 - 3.57156906 x10 * x13 + 3.40738932 x10 * x14 + 2.10591634 x10 * x17 - 2.10591634 x10 * x18 + x11^2 + 0.65916112 x11 * x12 + 2.50375742 x11 * x13 - 2 x11 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x17 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x17 - 0.65916112 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.5188787233 e151: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 6.67721368 x3 * x8 - 2.41729784 x3 * x15 + 2.41729784 x3 * x16 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 2.41729784 x4 * x8 + 6.67721368 x4 * x15 - 6.67721368 x4 * x16 + x5^2 - 2 x5 * x8 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 3.294577882 e152: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 6.67721368 x3 * x11 - 2.41729784 x3 * x15 + 2.41729784 x3 * x17 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 2.41729784 x4 * x11 + 6.67721368 x4 * x15 - 6.67721368 x4 * x17 + x5^2 - 2 x5 * x11 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 3.663483547 e153: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 6.67721368 x3 * x14 - 2.41729784 x3 * x15 + 2.41729784 x3 * x18 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 2.41729784 x4 * x14 + 6.67721368 x4 * x15 - 6.67721368 x4 * x18 + x5^2 - 2 x5 * x14 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 2.060062494 e154: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 16.39322121 x3 * x6 + 1.902407482 x3 * x7 - 6.67721368 x3 * x8 - 2.41729784 x3 * x15 + 2.41729784 x3 * x16 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 1.902407482 x4 * x6 - 16.39322121 x4 * x7 - 2.41729784 x4 * x8 + 6.67721368 x4 * x15 - 6.67721368 x4 * x16 + x5^2 - 4.5236206 x5 * x6 - 1.06782914 x5 * x7 - 2 x5 * x8 + 5.400850601 x6^2 + 4.5236206 x6 * x8 + 1.06782914 x6 * x15 - 1.06782914 x6 * x16 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 4.5236206 x7 * x15 + 4.5236206 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.641445946 e155: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 + 12.87500735 x3 * x9 - 10.24230914 x3 * x10 - 6.67721368 x3 * x11 - 2.41729784 x3 * x15 + 2.41729784 x3 * x17 + 12.60712784 x4^2 + 2.41729784 x4 * x5 + 10.24230914 x4 * x9 + 12.87500735 x4 * x10 - 2.41729784 x4 * x11 + 6.67721368 x4 * x15 - 6.67721368 x4 * x17 + x5^2 + 4.3914795 x5 * x9 - 1.47802734 x5 * x10 - 2 x5 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x15 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x15 - 4.3914795 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 1.380677264 e156: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 11.3177039 x3 * x12 + 0.2898345836 x3 * x13 - 6.67721368 x3 * x14 - 2.41729784 x3 * x15 + 2.41729784 x3 * x18 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 0.2898345836 x4 * x12 - 11.3177039 x4 * x13 - 2.41729784 x4 * x14 + 6.67721368 x4 * x15 - 6.67721368 x4 * x18 + x5^2 - 3.02492942 x5 * x12 - 1.00827778 x5 * x13 - 2 x5 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x15 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x15 + 3.02492942 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.8670457232 e157: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 + 11.63176181 x3 * x6 - 9.692686537 x3 * x7 - 6.67721368 x3 * x8 - 2.41729784 x3 * x15 + 2.41729784 x3 * x16 + 12.60712784 x4^2 + 2.41729784 x4 * x5 + 9.692686537 x4 * x6 + 11.63176181 x4 * x7 - 2.41729784 x4 * x8 + 6.67721368 x4 * x15 - 6.67721368 x4 * x16 + x5^2 + 4.009552 x5 * x6 - 1.45166714 x5 * x7 - 2 x5 * x8 + 4.545961182 x6^2 - 4.009552 x6 * x8 + 1.45166714 x6 * x15 - 1.45166714 x6 * x16 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 4.009552 x7 * x15 - 4.009552 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.186509699 e158: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 2.912489276 x3 * x9 + 13.9212468 x3 * x10 - 6.67721368 x3 * x11 - 2.41729784 x3 * x15 + 2.41729784 x3 * x17 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 13.9212468 x4 * x9 - 2.912489276 x4 * x10 - 2.41729784 x4 * x11 + 6.67721368 x4 * x15 - 6.67721368 x4 * x17 + x5^2 - 2.10591634 x5 * x9 + 3.40738932 x5 * x10 - 2 x5 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x15 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x15 + 2.10591634 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 0.7414420615 e159: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 + 5.783245525 x3 * x12 - 7.699093866 x3 * x13 - 6.67721368 x3 * x14 - 2.41729784 x3 * x15 + 2.41729784 x3 * x18 + 12.60712784 x4^2 + 2.41729784 x4 * x5 + 7.699093866 x4 * x12 + 5.783245525 x4 * x13 - 2.41729784 x4 * x14 + 6.67721368 x4 * x15 - 6.67721368 x4 * x18 + x5^2 + 2.26962754 x5 * x12 - 1.48442486 x5 * x13 - 2 x5 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x15 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x15 - 2.26962754 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.4803589854 e160: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 26.66148871 x3 * x6 + 3.093842271 x3 * x7 - 6.67721368 x3 * x8 - 2.41729784 x3 * x15 + 2.41729784 x3 * x16 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 3.093842271 x4 * x6 - 26.66148871 x4 * x7 - 2.41729784 x4 * x8 + 6.67721368 x4 * x15 - 6.67721368 x4 * x16 + x5^2 - 7.357076 x5 * x6 - 1.7367363 x5 * x7 - 2 x5 * x8 + 14.28570506 x6^2 + 7.357076 x6 * x8 + 1.7367363 x6 * x15 - 1.7367363 x6 * x16 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 7.357076 x7 * x15 + 7.357076 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 0.8963084478 e161: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 + 9.152705948 x3 * x9 - 5.985757533 x3 * x10 - 6.67721368 x3 * x11 - 2.41729784 x3 * x15 + 2.41729784 x3 * x17 + 12.60712784 x4^2 + 2.41729784 x4 * x5 + 5.985757533 x4 * x9 + 9.152705948 x4 * x10 - 2.41729784 x4 * x11 + 6.67721368 x4 * x15 - 6.67721368 x4 * x17 + x5^2 + 2.9976666 x5 * x9 - 0.70766974 x5 * x10 - 2 x5 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x15 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x15 - 2.9976666 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 2.434235804 e162: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 17.19660631 x3 * x12 + 0.4402537848 x3 * x13 - 6.67721368 x3 * x14 - 2.41729784 x3 * x15 + 2.41729784 x3 * x18 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 0.4402537848 x4 * x12 - 17.19660631 x4 * x13 - 2.41729784 x4 * x14 + 6.67721368 x4 * x15 - 6.67721368 x4 * x18 + x5^2 - 4.59619514 x5 * x12 - 1.53205596 x5 * x13 - 2 x5 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x15 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x15 + 4.59619514 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.4479140474 e163: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 33.09283459 x3 * x6 + 3.840229883 x3 * x7 - 6.67721368 x3 * x8 - 2.41729784 x3 * x15 + 2.41729784 x3 * x16 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 3.840229883 x4 * x6 - 33.09283459 x4 * x7 - 2.41729784 x4 * x8 + 6.67721368 x4 * x15 - 6.67721368 x4 * x16 + x5^2 - 9.1317749 x5 * x6 - 2.15565364 x5 * x7 - 2 x5 * x8 + 22.00903886 x6^2 + 9.1317749 x6 * x8 + 2.15565364 x6 * x15 - 2.15565364 x6 * x16 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 9.1317749 x7 * x15 + 9.1317749 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 0.5435738211 e164: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 - 11.51114752 x3 * x9 - 5.392049769 x3 * x10 - 6.67721368 x3 * x11 - 2.41729784 x3 * x15 + 2.41729784 x3 * x17 + 12.60712784 x4^2 + 2.41729784 x4 * x5 + 5.392049769 x4 * x9 - 11.51114752 x4 * x10 - 2.41729784 x4 * x11 + 6.67721368 x4 * x15 - 6.67721368 x4 * x17 + x5^2 - 2.5314331 x5 * x9 - 2.53149414 x5 * x10 - 2 x5 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x15 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x15 + 2.5314331 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 0.4202819597 e165: [ 12.60712784 x3^2 + 6.67721368 x3 * x5 + 5.226843526 x3 * x12 + 7.562367272 x3 * x13 - 6.67721368 x3 * x14 - 2.41729784 x3 * x15 + 2.41729784 x3 * x18 + 12.60712784 x4^2 + 2.41729784 x4 * x5 - 7.562367272 x4 * x12 + 5.226843526 x4 * x13 - 2.41729784 x4 * x14 + 6.67721368 x4 * x15 - 6.67721368 x4 * x18 + x5^2 + 0.65916112 x5 * x12 + 2.50375742 x5 * x13 - 2 x5 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x15 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x15 - 0.65916112 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.3989108671 e166: [ 14.28570506 x6^2 + 7.357076 x6 * x8 - 7.357076 x6 * x11 - 1.7367363 x6 * x16 + 1.7367363 x6 * x17 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 1.7367363 x7 * x11 + 7.357076 x7 * x16 - 7.357076 x7 * x17 + x8^2 - 2 x8 * x11 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 4.361526123 e167: [ 14.28570506 x6^2 + 7.357076 x6 * x8 - 7.357076 x6 * x14 - 1.7367363 x6 * x16 + 1.7367363 x6 * x18 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 1.7367363 x7 * x14 + 7.357076 x7 * x16 - 7.357076 x7 * x18 + x8^2 - 2 x8 * x14 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 2.591119989 e168: [ 14.28570506 x6^2 + 7.357076 x6 * x8 + 14.87075235 x6 * x9 - 9.250400664 x6 * x10 - 7.357076 x6 * x11 - 1.7367363 x6 * x16 + 1.7367363 x6 * x17 + 14.28570506 x7^2 + 1.7367363 x7 * x8 + 9.250400664 x7 * x9 + 14.87075235 x7 * x10 - 1.7367363 x7 * x11 + 7.357076 x7 * x16 - 7.357076 x7 * x17 + x8^2 + 4.3914795 x8 * x9 - 1.47802734 x8 * x10 - 2 x8 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x16 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x16 - 4.3914795 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 1.820950745 e169: [ 14.28570506 x6^2 + 7.357076 x6 * x8 - 12.00287413 x6 * x12 - 1.082235764 x6 * x13 - 7.357076 x6 * x14 - 1.7367363 x6 * x16 + 1.7367363 x6 * x18 + 14.28570506 x7^2 + 1.7367363 x7 * x8 + 1.082235764 x7 * x12 - 12.00287413 x7 * x13 - 1.7367363 x7 * x14 + 7.357076 x7 * x16 - 7.357076 x7 * x18 + x8^2 - 3.02492942 x8 * x12 - 1.00827778 x8 * x13 - 2 x8 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x16 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x16 + 3.02492942 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.222255705 e170: [ 14.28570506 x6^2 + 7.357076 x6 * x8 - 4.787824921 x6 * x9 + 14.36292177 x6 * x10 - 7.357076 x6 * x11 - 1.7367363 x6 * x16 + 1.7367363 x6 * x17 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 14.36292177 x7 * x9 - 4.787824921 x7 * x10 - 1.7367363 x7 * x11 + 7.357076 x7 * x16 - 7.357076 x7 * x17 + x8^2 - 2.10591634 x8 * x9 + 3.40738932 x8 * x10 - 2 x8 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x16 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x16 + 2.10591634 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 1.072206695 e171: [ 14.28570506 x6^2 + 7.357076 x6 * x8 + 7.059883882 x6 * x12 - 7.431385524 x6 * x13 - 7.357076 x6 * x14 - 1.7367363 x6 * x16 + 1.7367363 x6 * x18 + 14.28570506 x7^2 + 1.7367363 x7 * x8 + 7.431385524 x7 * x12 + 7.059883882 x7 * x13 - 1.7367363 x7 * x14 + 7.357076 x7 * x16 - 7.357076 x7 * x18 + x8^2 + 2.26962754 x8 * x12 - 1.48442486 x8 * x13 - 2 x8 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x16 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x16 - 2.26962754 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.7525270849 e172: [ 14.28570506 x6^2 + 7.357076 x6 * x8 + 10.41251264 x6 * x9 - 5.20626823 x6 * x10 - 7.357076 x6 * x11 - 1.7367363 x6 * x16 + 1.7367363 x6 * x17 + 14.28570506 x7^2 + 1.7367363 x7 * x8 + 5.20626823 x7 * x9 + 10.41251264 x7 * x10 - 1.7367363 x7 * x11 + 7.357076 x7 * x16 - 7.357076 x7 * x17 + x8^2 + 2.9976666 x8 * x9 - 0.70766974 x8 * x10 - 2 x8 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x16 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x16 - 2.9976666 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 3.008863561 e173: [ 14.28570506 x6^2 + 7.357076 x6 * x8 - 18.23766708 x6 * x12 - 1.644536596 x6 * x13 - 7.357076 x6 * x14 - 1.7367363 x6 * x16 + 1.7367363 x6 * x18 + 14.28570506 x7^2 + 1.7367363 x7 * x8 + 1.644536596 x7 * x12 - 18.23766708 x7 * x13 - 1.7367363 x7 * x14 + 7.357076 x7 * x16 - 7.357076 x7 * x18 + x8^2 - 4.59619514 x8 * x12 - 1.53205596 x8 * x13 - 2 x8 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x16 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x16 + 4.59619514 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.7117751037 e174: [ 14.28570506 x6^2 + 7.357076 x6 * x8 - 11.51024174 x6 * x9 - 7.113981513 x6 * x10 - 7.357076 x6 * x11 - 1.7367363 x6 * x16 + 1.7367363 x6 * x17 + 14.28570506 x7^2 + 1.7367363 x7 * x8 + 7.113981513 x7 * x9 - 11.51024174 x7 * x10 - 1.7367363 x7 * x11 + 7.357076 x7 * x16 - 7.357076 x7 * x17 + x8^2 - 2.5314331 x8 * x9 - 2.53149414 x8 * x10 - 2 x8 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x16 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x16 + 2.5314331 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 0.6768277376 e175: [ 14.28570506 x6^2 + 7.357076 x6 * x8 + 4.598932427 x6 * x12 + 8.63777229 x6 * x13 - 7.357076 x6 * x14 - 1.7367363 x6 * x16 + 1.7367363 x6 * x18 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 8.63777229 x7 * x12 + 4.598932427 x7 * x13 - 1.7367363 x7 * x14 + 7.357076 x7 * x16 - 7.357076 x7 * x18 + x8^2 + 0.65916112 x8 * x12 + 2.50375742 x8 * x13 - 2 x8 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x16 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x16 - 0.65916112 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.649632373 e176: [ 2.371700376 x9^2 - 2.9976666 x9 * x11 + 2.9976666 x9 * x14 - 0.70766974 x9 * x17 + 0.70766974 x9 * x18 + 2.371700376 x10^2 + 0.70766974 x10 * x11 - 0.70766974 x10 * x14 - 2.9976666 x10 * x17 + 2.9976666 x10 * x18 + x11^2 - 2 x11 * x14 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 4.942456881 e177: [ 2.371700376 x9^2 - 2.9976666 x9 * x11 + 4.177101108 x9 * x12 + 2.58156582 x9 * x13 + 2.9976666 x9 * x14 - 0.70766974 x9 * x17 + 0.70766974 x9 * x18 + 2.371700376 x10^2 + 0.70766974 x10 * x11 - 2.58156582 x10 * x12 + 4.177101108 x10 * x13 - 0.70766974 x10 * x14 - 2.9976666 x10 * x17 + 2.9976666 x10 * x18 + x11^2 - 3.02492942 x11 * x12 - 1.00827778 x11 * x13 - 2 x11 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x17 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x17 + 3.02492942 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 2.955046366 e178: [ 2.371700376 x9^2 - 2.9976666 x9 * x11 - 3.927034613 x9 * x12 + 1.421832046 x9 * x13 + 2.9976666 x9 * x14 - 0.70766974 x9 * x17 + 0.70766974 x9 * x18 + 2.371700376 x10^2 + 0.70766974 x10 * x11 - 1.421832046 x10 * x12 - 3.927034613 x10 * x13 - 0.70766974 x10 * x14 - 2.9976666 x10 * x17 + 2.9976666 x10 * x18 + x11^2 + 2.26962754 x11 * x12 - 1.48442486 x11 * x13 - 2 x11 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x17 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x17 - 2.26962754 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 2.193216694 e179: [ 2.371700376 x9^2 - 2.9976666 x9 * x11 + 6.346835508 x9 * x12 + 3.9225906 x9 * x13 + 2.9976666 x9 * x14 - 0.70766974 x9 * x17 + 0.70766974 x9 * x18 + 2.371700376 x10^2 + 0.70766974 x10 * x11 - 3.9225906 x10 * x12 + 6.346835508 x10 * x13 - 0.70766974 x10 * x14 - 2.9976666 x10 * x17 + 2.9976666 x10 * x18 + x11^2 - 4.59619514 x11 * x12 - 1.53205596 x11 * x13 - 2 x11 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x17 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x17 + 4.59619514 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 2.123244565 e180: [ 2.371700376 x9^2 - 2.9976666 x9 * x11 - 0.1020559555 x9 * x12 - 3.985949185 x9 * x13 + 2.9976666 x9 * x14 - 0.70766974 x9 * x17 + 0.70766974 x9 * x18 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 3.985949185 x10 * x12 - 0.1020559555 x10 * x13 - 0.70766974 x10 * x14 - 2.9976666 x10 * x17 + 2.9976666 x10 * x18 + x11^2 + 0.65916112 x11 * x12 + 2.50375742 x11 * x13 - 2 x11 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x17 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x17 - 0.65916112 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 2.014883271 e181: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 0.33813906 x3 * x8 + 3.721697 x3 * x15 - 3.721697 x3 * x16 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 3.721697 x4 * x8 - 0.33813906 x4 * x15 + 0.33813906 x4 * x16 + x5^2 - 2 x5 * x8 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 2.898849893 e182: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 0.33813906 x3 * x11 + 3.721697 x3 * x15 - 3.721697 x3 * x17 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 3.721697 x4 * x11 - 0.33813906 x4 * x15 + 0.33813906 x4 * x17 + x5^2 - 2 x5 * x11 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 3.245498018 e183: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 0.33813906 x3 * x14 + 3.721697 x3 * x15 - 3.721697 x3 * x18 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 3.721697 x4 * x14 - 0.33813906 x4 * x15 + 0.33813906 x4 * x18 + x5^2 - 2 x5 * x14 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 1.749787908 e184: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 2.751874662 x3 * x6 - 8.237235237 x3 * x7 + 0.33813906 x3 * x8 + 3.721697 x3 * x15 - 3.721697 x3 * x16 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 8.237235237 x4 * x6 + 2.751874662 x4 * x7 + 3.721697 x4 * x8 - 0.33813906 x4 * x15 + 0.33813906 x4 * x16 + x5^2 - 4.5236206 x5 * x6 - 1.06782914 x5 * x7 - 2 x5 * x8 + 5.400850601 x6^2 + 4.5236206 x6 * x8 + 1.06782914 x6 * x15 - 1.06782914 x6 * x16 + 5.400850601 x7^2 + 1.06782914 x7 * x8 - 4.5236206 x7 * x15 + 4.5236206 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 1.365843282 e185: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 2.007919584 x3 * x9 + 8.421767428 x3 * x10 + 0.33813906 x3 * x11 + 3.721697 x3 * x15 - 3.721697 x3 * x17 + 3.491341646 x4^2 - 3.721697 x4 * x5 - 8.421767428 x4 * x9 + 2.007919584 x4 * x10 + 3.721697 x4 * x11 - 0.33813906 x4 * x15 + 0.33813906 x4 * x17 + x5^2 + 4.3914795 x5 * x9 - 1.47802734 x5 * x10 - 2 x5 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x15 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x15 - 4.3914795 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 1.128961394 e186: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 2.38767559 x3 * x12 - 5.458466323 x3 * x13 + 0.33813906 x3 * x14 + 3.721697 x3 * x15 - 3.721697 x3 * x18 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 5.458466323 x4 * x12 + 2.38767559 x4 * x13 + 3.721697 x4 * x14 - 0.33813906 x4 * x15 + 0.33813906 x4 * x18 + x5^2 - 3.02492942 x5 * x12 - 1.00827778 x5 * x13 - 2 x5 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x15 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x15 + 3.02492942 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.6701986451 e187: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 2.023439548 x3 * x6 + 7.706601506 x3 * x7 + 0.33813906 x3 * x8 + 3.721697 x3 * x15 - 3.721697 x3 * x16 + 3.491341646 x4^2 - 3.721697 x4 * x5 - 7.706601506 x4 * x6 + 2.023439548 x4 * x7 + 3.721697 x4 * x8 - 0.33813906 x4 * x15 + 0.33813906 x4 * x16 + x5^2 + 4.009552 x5 * x6 - 1.45166714 x5 * x7 - 2 x5 * x8 + 4.545961182 x6^2 - 4.009552 x6 * x8 + 1.45166714 x6 * x15 - 1.45166714 x6 * x16 + 4.545961182 x7^2 + 1.45166714 x7 * x8 + 4.009552 x7 * x15 - 4.009552 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 0.9540873885 e188: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 - 5.984589019 x3 * x9 - 4.494876973 x3 * x10 + 0.33813906 x3 * x11 + 3.721697 x3 * x15 - 3.721697 x3 * x17 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 4.494876973 x4 * x9 - 5.984589019 x4 * x10 + 3.721697 x4 * x11 - 0.33813906 x4 * x15 + 0.33813906 x4 * x17 + x5^2 - 2.10591634 x5 * x9 + 3.40738932 x5 * x10 - 2 x5 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x15 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x15 + 2.10591634 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 0.5603630484 e189: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 2.378564913 x3 * x12 + 4.474404017 x3 * x13 + 0.33813906 x3 * x14 + 3.721697 x3 * x15 - 3.721697 x3 * x18 + 3.491341646 x4^2 - 3.721697 x4 * x5 - 4.474404017 x4 * x12 + 2.378564913 x4 * x13 + 3.721697 x4 * x14 - 0.33813906 x4 * x15 + 0.33813906 x4 * x18 + x5^2 + 2.26962754 x5 * x12 - 1.48442486 x5 * x13 - 2 x5 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x15 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x15 - 2.26962754 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.3370766896 e190: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 4.47566052 x3 * x6 - 13.39677465 x3 * x7 + 0.33813906 x3 * x8 + 3.721697 x3 * x15 - 3.721697 x3 * x16 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 13.39677465 x4 * x6 + 4.47566052 x4 * x7 + 3.721697 x4 * x8 - 0.33813906 x4 * x15 + 0.33813906 x4 * x16 + x5^2 - 7.357076 x5 * x6 - 1.7367363 x5 * x7 - 2 x5 * x8 + 14.28570506 x6^2 + 7.357076 x6 * x8 + 1.7367363 x6 * x15 - 1.7367363 x6 * x16 + 14.28570506 x7^2 + 1.7367363 x7 * x8 - 7.357076 x7 * x15 + 7.357076 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 0.6959553598 e191: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 0.810052091 x3 * x9 + 5.697848786 x3 * x10 + 0.33813906 x3 * x11 + 3.721697 x3 * x15 - 3.721697 x3 * x17 + 3.491341646 x4^2 - 3.721697 x4 * x5 - 5.697848786 x4 * x9 + 0.810052091 x4 * x10 + 3.721697 x4 * x11 - 0.33813906 x4 * x15 + 0.33813906 x4 * x17 + x5^2 + 2.9976666 x5 * x9 - 0.70766974 x5 * x10 - 2 x5 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x15 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x15 - 2.9976666 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 2.095856948 e192: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 3.628000587 x3 * x12 - 8.293798851 x3 * x13 + 0.33813906 x3 * x14 + 3.721697 x3 * x15 - 3.721697 x3 * x18 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 8.293798851 x4 * x12 + 3.628000587 x4 * x13 + 3.721697 x4 * x14 - 0.33813906 x4 * x15 + 0.33813906 x4 * x18 + x5^2 - 4.59619514 x5 * x12 - 1.53205596 x5 * x13 - 2 x5 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x15 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x15 + 4.59619514 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.3099900713 e193: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 5.555249733 x3 * x6 - 16.62839428 x3 * x7 + 0.33813906 x3 * x8 + 3.721697 x3 * x15 - 3.721697 x3 * x16 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 16.62839428 x4 * x6 + 5.555249733 x4 * x7 + 3.721697 x4 * x8 - 0.33813906 x4 * x15 + 0.33813906 x4 * x16 + x5^2 - 9.1317749 x5 * x6 - 2.15565364 x5 * x7 - 2 x5 * x8 + 22.00903886 x6^2 + 9.1317749 x6 * x8 + 2.15565364 x6 * x15 - 2.15565364 x6 * x16 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 9.1317749 x7 * x15 + 9.1317749 x7 * x16 + x8^2 + x15^2 - 2 x15 * x16 + x16^2 ] >= 0.3903479242 e194: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 + 5.138715278 x3 * x9 - 4.282614963 x3 * x10 + 0.33813906 x3 * x11 + 3.721697 x3 * x15 - 3.721697 x3 * x17 + 3.491341646 x4^2 - 3.721697 x4 * x5 + 4.282614963 x4 * x9 + 5.138715278 x4 * x10 + 3.721697 x4 * x11 - 0.33813906 x4 * x15 + 0.33813906 x4 * x17 + x5^2 - 2.5314331 x5 * x9 - 2.53149414 x5 * x10 - 2 x5 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x15 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x15 + 2.5314331 x10 * x17 + x11^2 + x15^2 - 2 x15 * x17 + x17^2 ] >= 0.2870765821 e195: [ 3.491341646 x3^2 - 0.33813906 x3 * x5 - 4.7705573 x3 * x12 + 0.8032898912 x3 * x13 + 0.33813906 x3 * x14 + 3.721697 x3 * x15 - 3.721697 x3 * x18 + 3.491341646 x4^2 - 3.721697 x4 * x5 - 0.8032898912 x4 * x12 - 4.7705573 x4 * x13 + 3.721697 x4 * x14 - 0.33813906 x4 * x15 + 0.33813906 x4 * x18 + x5^2 + 0.65916112 x5 * x12 + 2.50375742 x5 * x13 - 2 x5 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x15 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x15 - 0.65916112 x13 * x18 + x14^2 + x15^2 - 2 x15 * x18 + x18^2 ] >= 0.2694623391 e196: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 - 9.1317749 x6 * x11 - 2.15565364 x6 * x16 + 2.15565364 x6 * x17 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 2.15565364 x7 * x11 + 9.1317749 x7 * x16 - 9.1317749 x7 * x17 + x8^2 - 2 x8 * x11 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 3.530511801 e197: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 - 9.1317749 x6 * x14 - 2.15565364 x6 * x16 + 2.15565364 x6 * x18 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 2.15565364 x7 * x14 + 9.1317749 x7 * x16 - 9.1317749 x7 * x18 + x8^2 - 2 x8 * x14 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 1.960656739 e198: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 + 18.45794363 x6 * x9 - 11.48176087 x6 * x10 - 9.1317749 x6 * x11 - 2.15565364 x6 * x16 + 2.15565364 x6 * x17 + 22.00903886 x7^2 + 2.15565364 x7 * x8 + 11.48176087 x7 * x9 + 18.45794363 x7 * x10 - 2.15565364 x7 * x11 + 9.1317749 x7 * x16 - 9.1317749 x7 * x17 + x8^2 + 4.3914795 x8 * x9 - 1.47802734 x8 * x10 - 2 x8 * x11 + 5.367414254 x9^2 - 4.3914795 x9 * x11 + 1.47802734 x9 * x16 - 1.47802734 x9 * x17 + 5.367414254 x10^2 + 1.47802734 x10 * x11 + 4.3914795 x10 * x16 - 4.3914795 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 1.299520178 e199: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 - 14.89823611 x6 * x12 - 1.343332804 x6 * x13 - 9.1317749 x6 * x14 - 2.15565364 x6 * x16 + 2.15565364 x6 * x18 + 22.00903886 x7^2 + 2.15565364 x7 * x8 + 1.343332804 x7 * x12 - 14.89823611 x7 * x13 - 2.15565364 x7 * x14 + 9.1317749 x7 * x16 - 9.1317749 x7 * x18 + x8^2 - 3.02492942 x8 * x12 - 1.00827778 x8 * x13 - 2 x8 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x16 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x16 + 3.02492942 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.8029874139 e200: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 - 5.942801392 x6 * x9 + 17.82756925 x6 * x10 - 9.1317749 x6 * x11 - 2.15565364 x6 * x16 + 2.15565364 x6 * x17 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 17.82756925 x7 * x9 - 5.942801392 x7 * x10 - 2.15565364 x7 * x11 + 9.1317749 x7 * x16 - 9.1317749 x7 * x17 + x8^2 - 2.10591634 x8 * x9 + 3.40738932 x8 * x10 - 2 x8 * x11 + 4.011296402 x9^2 + 2.10591634 x9 * x11 - 3.40738932 x9 * x16 + 3.40738932 x9 * x17 + 4.011296402 x10^2 - 3.40738932 x10 * x11 - 2.10591634 x10 * x16 + 2.10591634 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 0.6822975588 e201: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 + 8.762910975 x6 * x12 - 9.223982273 x6 * x13 - 9.1317749 x6 * x14 - 2.15565364 x6 * x16 + 2.15565364 x6 * x18 + 22.00903886 x7^2 + 2.15565364 x7 * x8 + 9.223982273 x7 * x12 + 8.762910975 x7 * x13 - 2.15565364 x7 * x14 + 9.1317749 x7 * x16 - 9.1317749 x7 * x18 + x8^2 + 2.26962754 x8 * x12 - 1.48442486 x8 * x13 - 2 x8 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x16 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x16 - 2.26962754 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.4329930841 e202: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 + 12.92426288 x6 * x9 - 6.462105844 x6 * x10 - 9.1317749 x6 * x11 - 2.15565364 x6 * x16 + 2.15565364 x6 * x17 + 22.00903886 x7^2 + 2.15565364 x7 * x8 + 6.462105844 x7 * x9 + 12.92426288 x7 * x10 - 2.15565364 x7 * x11 + 9.1317749 x7 * x16 - 9.1317749 x7 * x17 + x8^2 + 2.9976666 x8 * x9 - 0.70766974 x8 * x10 - 2 x8 * x11 + 2.371700376 x9^2 - 2.9976666 x9 * x11 + 0.70766974 x9 * x16 - 0.70766974 x9 * x17 + 2.371700376 x10^2 + 0.70766974 x10 * x11 + 2.9976666 x10 * x16 - 2.9976666 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 2.326071907 e203: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 - 22.63700071 x6 * x12 - 2.041292689 x6 * x13 - 9.1317749 x6 * x14 - 2.15565364 x6 * x16 + 2.15565364 x6 * x18 + 22.00903886 x7^2 + 2.15565364 x7 * x8 + 2.041292689 x7 * x12 - 22.63700071 x7 * x13 - 2.15565364 x7 * x14 + 9.1317749 x7 * x16 - 9.1317749 x7 * x18 + x8^2 - 4.59619514 x8 * x12 - 1.53205596 x8 * x13 - 2 x8 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x16 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x16 + 4.59619514 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.4022179607 e204: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 - 14.2867509 x6 * x9 - 8.830070835 x6 * x10 - 9.1317749 x6 * x11 - 2.15565364 x6 * x16 + 2.15565364 x6 * x17 + 22.00903886 x7^2 + 2.15565364 x7 * x8 + 8.830070835 x7 * x9 - 14.2867509 x7 * x10 - 2.15565364 x7 * x11 + 9.1317749 x7 * x16 - 9.1317749 x7 * x17 + x8^2 - 2.5314331 x8 * x9 - 2.53149414 x8 * x10 - 2 x8 * x11 + 3.20415403 x9^2 + 2.5314331 x9 * x11 + 2.53149414 x9 * x16 - 2.53149414 x9 * x17 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.5314331 x10 * x16 + 2.5314331 x10 * x17 + x11^2 + x16^2 - 2 x16 * x17 + x17^2 ] >= 0.3760563312 e205: [ 22.00903886 x6^2 + 9.1317749 x6 * x8 + 5.708272383 x6 * x12 + 10.72141305 x6 * x13 - 9.1317749 x6 * x14 - 2.15565364 x6 * x16 + 2.15565364 x6 * x18 + 22.00903886 x7^2 + 2.15565364 x7 * x8 - 10.72141305 x7 * x12 + 5.708272383 x7 * x13 - 2.15565364 x7 * x14 + 9.1317749 x7 * x16 - 9.1317749 x7 * x18 + x8^2 + 0.65916112 x8 * x12 + 2.50375742 x8 * x13 - 2 x8 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x16 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x16 - 0.65916112 x13 * x18 + x14^2 + x16^2 - 2 x16 * x18 + x18^2 ] >= 0.3558559867 e206: [ 3.20415403 x9^2 + 2.5314331 x9 * x11 - 2.5314331 x9 * x14 - 2.53149414 x9 * x17 + 2.53149414 x9 * x18 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.53149414 x10 * x14 + 2.5314331 x10 * x17 - 2.5314331 x10 * x18 + x11^2 - 2 x11 * x14 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 1.719380522 e207: [ 3.20415403 x9^2 + 2.5314331 x9 * x11 - 5.104927875 x9 * x12 + 2.552601677 x9 * x13 - 2.5314331 x9 * x14 - 2.53149414 x9 * x17 + 2.53149414 x9 * x18 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.552601677 x10 * x12 - 5.104927875 x10 * x13 - 2.53149414 x10 * x14 + 2.5314331 x10 * x17 - 2.5314331 x10 * x18 + x11^2 - 3.02492942 x11 * x12 - 1.00827778 x11 * x13 - 2 x11 * x14 + 2.541705519 x12^2 + 3.02492942 x12 * x14 + 1.00827778 x12 * x17 - 1.00827778 x12 * x18 + 2.541705519 x13^2 + 1.00827778 x13 * x14 - 3.02492942 x13 * x17 + 3.02492942 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.6514307975 e208: [ 3.20415403 x9^2 + 2.5314331 x9 * x11 + 0.9937987225 x9 * x12 - 4.751635521 x9 * x13 - 2.5314331 x9 * x14 - 2.53149414 x9 * x17 + 2.53149414 x9 * x18 + 3.20415403 x10^2 + 2.53149414 x10 * x11 + 4.751635521 x10 * x12 + 0.9937987225 x10 * x13 - 2.53149414 x10 * x14 + 2.5314331 x10 * x17 - 2.5314331 x10 * x18 + x11^2 + 2.26962754 x11 * x12 - 1.48442486 x11 * x13 - 2 x11 * x14 + 1.838681584 x12^2 - 2.26962754 x12 * x14 + 1.48442486 x12 * x17 - 1.48442486 x12 * x18 + 1.838681584 x13^2 + 1.48442486 x13 * x14 + 2.26962754 x13 * x17 - 2.26962754 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.3238054746 e209: [ 3.20415403 x9^2 + 2.5314331 x9 * x11 - 7.756675598 x9 * x12 + 3.878471948 x9 * x13 - 2.5314331 x9 * x14 - 2.53149414 x9 * x17 + 2.53149414 x9 * x18 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 3.878471948 x10 * x12 - 7.756675598 x10 * x13 - 2.53149414 x10 * x14 + 2.5314331 x10 * x17 - 2.5314331 x10 * x18 + x11^2 - 4.59619514 x11 * x12 - 1.53205596 x11 * x13 - 2 x11 * x14 + 5.868051307 x12^2 + 4.59619514 x12 * x14 + 1.53205596 x12 * x17 - 1.53205596 x12 * x18 + 5.868051307 x13^2 + 1.53205596 x13 * x14 - 4.59619514 x13 * x17 + 4.59619514 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.2972687086 e210: [ 3.20415403 x9^2 + 2.5314331 x9 * x11 + 4.003434757 x9 * x12 + 2.334715947 x9 * x13 - 2.5314331 x9 * x14 - 2.53149414 x9 * x17 + 2.53149414 x9 * x18 + 3.20415403 x10^2 + 2.53149414 x10 * x11 - 2.334715947 x10 * x12 + 4.003434757 x10 * x13 - 2.53149414 x10 * x14 + 2.5314331 x10 * x17 - 2.5314331 x10 * x18 + x11^2 + 0.65916112 x11 * x12 + 2.50375742 x11 * x13 - 2 x11 * x14 + 1.67582365 x12^2 - 0.65916112 x12 * x14 - 2.50375742 x12 * x17 + 2.50375742 x12 * x18 + 1.67582365 x13^2 - 2.50375742 x13 * x14 + 0.65916112 x13 * x17 - 0.65916112 x13 * x18 + x14^2 + x17^2 - 2 x17 * x18 + x18^2 ] >= 0.2576106975 Bounds x2 <= 6 -1 <= x3 <= 1 -1 <= x4 <= 1 1.59481484 <= x5 <= 4.40518516 -1 <= x6 <= 1 x7 <= 1 1.42893129 <= x8 <= 4.57106871 -1 <= x9 <= 1 -1 <= x10 <= 1 1.52785695 <= x11 <= 4.47214305 -1 <= x12 <= 1 -1 <= x13 <= 1 1.04912586 <= x14 <= 4.95087414 1.59481484 <= x15 <= 8.40518516 1.42893129 <= x16 <= 8.57106871 1.52785695 <= x17 <= 8.47214305 1.04912586 <= x18 <= 8.95087414 End