「……でも、これって何のメリットがあるんだ？」

俺は、Case. 1 を選んだ。

わざわざ、F_5 で考えるくらいなんだから、何かそれなりの理由があるのだろう。

「鈍感。例えば、係数が膨張しないことが挙げられるだろう。」

「膨張？」

「適当。一般に、複素数体でのグレブナー基底では、3や7などの小さな整数に限らず、234/337、323423/13947 などの複雑な有理数が出てくる可能性がある。」

「ああ、確かにそうだな。」

「一方。F_5 は、{0,1,2,3,4} の中での計算しかないから、絶対に、桁数が大きくなったりしない。」

「あ、なるほど！」

「ただし。今回のケースで、それが効率的な計算につながるかは、実験してみないと分からないが。」

南條はそう言って、お冷に入っていた氷を、パクッと口に入れた。

「では。実際に、F_5 でグレブナー基底を計算してみよう。」

南條は、パソコンを取り出して、Mathematica を起動した。

「まず。これが、この前、本条が計算していた、東京、千葉、神奈川、埼玉、山梨、静岡、長野を塗り分けるグレブナー基底、だ。」

南條が、

GroebnerBasis[{x1^4 - 1, x2^4 - 1, x3^4 - 1, x4^4 - 1, x5^4 - 1, x6^4 - 1, x7^4 - 1, (x1 + x2)*(x1^2 + x2^2), (x1 + x3)*(x1^2 + x3^2), (x1 + x4)*(x1^2 + x4^2), (x1 + x5)*(x1^2 + x5^2), (x2 + x4)*(x1^2 + x4^2), (x4 + x5)*(x4^2 + x5^2), (x4 + x7)*(x4^2 + x7^2), (x3 + x5)*(x3^2 + x5^2), (x3 + x6)*(x3^2 + x6^2), (x5 + x6)*(x5^2 + x6^2), (x5 + x7)*(x5^2 + x7^2), (x6 + x7)*(x6^2 + x7^2)}, {x1, x2, x3, x4, x5, x6, x7}]

を入力し、Shift+Enter を押すと、

{-1 + x7^4, x6^3 + x6^2 x7 + x6 x7^2 + x7^3, x5^2 + x5 x6 + x6^2 + x5 x7 + x6 x7 + x7^2, x4^2 + x4 x5 - x5 x6 - x6^2 + x4 x7 - x6 x7, x3 x5 x6 + x3 x6^2 + x5 x6^2 + x3 x5 x7 + x3 x6 x7 + x5 x6 x7 - x6 x7^2 - x7^3, -1 + x3 x4 x6^2 + x3 x6^2 x7 - x4 x6^2 x7 + x3 x4 x7^2 + 2 x3 x5 x7^2 + 2 x3 x6 x7^2 + 2 x5 x6 x7^2 + x6^2 x7^2 + x3 x7^3 - x4 x7^3, x3 x4 x5 + x3 x4 x6 + x4 x5 x6 - x3 x6^2 + x4 x6^2 - x3 x5 x7 - x3 x6 x7 - x5 x6 x7 - x3 x7^2 + x7^3, x3^2 + x3 x5 + x3 x6 - x5 x7 - x6 x7 - x7^2, 1 - x2^2 x3 x4 - x2^2 x3 x5 + x2^3 x6 - x2^2 x3 x6 - x2^2 x4 x6 - 2 x2^2 x5 x6 + x2 x4 x5 x6 - x2^2 x6^2 - x2 x5 x6^2 + x4 x5 x6^2 + x2^3 x7 - x2^2 x3 x7 - x2^2 x5 x7 + x2 x4 x5 x7 - x2^2 x6 x7 + x2 x4 x6 x7 - x2 x5 x6 x7 + x4 x5 x6 x7 - x2 x6^2 x7 + x4 x6^2 x7 + x2 x4 x7^2 - x3 x4 x7^2 - x3 x5 x7^2 - x3 x6 x7^2 - x5 x6 x7^2 - x6^2 x7^2 + x2 x7^3 - x3 x7^3, -1 + x2^3 x4 + x2^3 x5 - x2^2 x4 x5 + x2^2 x5 x6 - x2 x4 x5 x6 + x2^2 x6^2 - x2 x4 x6^2 + x2^2 x5 x7 - x2 x4 x5 x7 + x2^2 x6 x7 - x2 x4 x6 x7 + x2 x5 x6 x7 - x4 x5 x6 x7 + x2 x6^2 x7 - x4 x6^2 x7 + x2^2 x7^2 - x2 x4 x7^2 + x2 x6 x7^2 - x4 x6 x7^2, x2^3 x3 + x2^3 x5 - x2^2 x4 x5 + x2^2 x3 x6 - x2 x3 x4 x6 + 2 x2^2 x5 x6 - 2 x2 x4 x5 x6 + 2 x2^2 x6^2 + x2 x3 x6^2 - 2 x2 x4 x6^2 + x2 x5 x6^2 - x4 x5 x6^2 - x2^2 x4 x7 + x2 x3 x4 x7 + 2 x2 x3 x5 x7 + x2^2 x6 x7 + x2 x3 x6 x7 - x2 x4 x6 x7 + x3 x4 x6 x7 + 2 x2 x5 x6 x7 - x3 x6^2 x7 + x4 x6^2 x7 + x2 x3 x7^2 -x2 x4 x7^2 + x3 x4 x7^2 - x2 x6 x7^2 + x4 x6 x7^2 + x6^2 x7^2 - 3 x2 x7^3 + x4 x7^3, -1 + x2^4, x3 x4 + x3 x5 + x1 x6 + x3 x6 + x4 x6 + 2 x5 x6 + x6^2 + x1 x7 + x3 x7 + x5 x7 + x6 x7, x1 x4 + x1 x5 + x4 x5 - x5 x6 - x6^2 - x5 x7 - x6 x7 - x7^2, x1 x3 + x1 x5 + x4 x5 - x3 x6 - 2 x5 x6 - 2 x6^2 + x4 x7 - x6 x7, x1 x2^2 + x2^3 + x2 x4 x5 - x2 x5 x6 + x4 x5 x6 - x2 x6^2 + x4 x6^2 + x2 x4 x7 - x2 x6 x7 + x4 x6 x7 + x1 x7^2 + x4 x7^2 + x5 x7^2 + x7^3, x1^2 - x4 x5 + x5 x6 + x6^2 - x4 x7 + x6 x7}

が出力された。

「確認。Mathematica では、デフォルトで、有理数体上でのグレブナー基底が計算される。」

「ああ。」

「つまり。今、多項式と変数順序の他に、何も入力しなかったので、有理数体上でのグレブナー基底が計算された。これを、F_5 上で計算するには、オプションでそれを指定する必要がある。」

「ええと、Modulus -> 5 とかだっけ？」

「適切。」

先ほどの入力の一番最後に、"Modulus -> 5" が付け加えられた。

「一般に。Modulus -> p で、F_p 上のグレブナー基底が計算できる。それでは、F_5 上で計算してみよう。」

{4 + x7^4, x6^3 + x6^2 x7 + x6 x7^2 + x7^3, x5^2 + x5 x6 + x6^2 + x5 x7 + x6 x7 + x7^2, x4^2 + x4 x5 + 4 x5 x6 + 4 x6^2 + x4 x7 + 4 x6 x7, x3 x5 x6 + x3 x6^2 + x5 x6^2 + x3 x5 x7 + x3 x6 x7 + x5 x6 x7 + 4 x6 x7^2 + 4 x7^3, 4 + x3 x4 x6^2 + x3 x6^2 x7 + 4 x4 x6^2 x7 + x3 x4 x7^2 + 2 x3 x5 x7^2 + 2 x3 x6 x7^2 + 2 x5 x6 x7^2 + x6^2 x7^2 + x3 x7^3 + 4 x4 x7^3, x3 x4 x5 + x3 x4 x6 + x4 x5 x6 + 4 x3 x6^2 + x4 x6^2 + 4 x3 x5 x7 + 4 x3 x6 x7 + 4 x5 x6 x7 + 4 x3 x7^2 + x7^3, x3^2 + x3 x5 + x3 x6 + 4 x5 x7 + 4 x6 x7 + 4 x7^2, 1 + 4 x2^2 x3 x4 + 4 x2^2 x3 x5 + x2^3 x6 + 4 x2^2 x3 x6 + 4 x2^2 x4 x6 + 3 x2^2 x5 x6 + x2 x4 x5 x6 + 4 x2^2 x6^2 + 4 x2 x5 x6^2 + x4 x5 x6^2 + x2^3 x7 + 4 x2^2 x3 x7 + 4 x2^2 x5 x7 + x2 x4 x5 x7 + 4 x2^2 x6 x7 + x2 x4 x6 x7 + 4 x2 x5 x6 x7 + x4 x5 x6 x7 + 4 x2 x6^2 x7 + x4 x6^2 x7 + x2 x4 x7^2 + 4 x3 x4 x7^2 + 4 x3 x5 x7^2 + 4 x3 x6 x7^2 + 4 x5 x6 x7^2 + 4 x6^2 x7^2 + x2 x7^3 + 4 x3 x7^3, 4 + x2^3 x4 + x2^3 x5 + 4 x2^2 x4 x5 + x2^2 x5 x6 + 4 x2 x4 x5 x6 + x2^2 x6^2 + 4 x2 x4 x6^2 + x2^2 x5 x7 + 4 x2 x4 x5 x7 + x2^2 x6 x7 + 4 x2 x4 x6 x7 + x2 x5 x6 x7 + 4 x4 x5 x6 x7 + x2 x6^2 x7 + 4 x4 x6^2 x7 + x2^2 x7^2 + 4 x2 x4 x7^2 + x2 x6 x7^2 + 4 x4 x6 x7^2, x2^3 x3 + x2^3 x5 + 4 x2^2 x4 x5 + x2^2 x3 x6 + 4 x2 x3 x4 x6 + 2 x2^2 x5 x6 + 3 x2 x4 x5 x6 + 2 x2^2 x6^2 + x2 x3 x6^2 + 3 x2 x4 x6^2 + x2 x5 x6^2 + 4 x4 x5 x6^2 + 4 x2^2 x4 x7 + x2 x3 x4 x7 + 2 x2 x3 x5 x7 + x2^2 x6 x7 + x2 x3 x6 x7 + 4 x2 x4 x6 x7 + x3 x4 x6 x7 + 2 x2 x5 x6 x7 + 4 x3 x6^2 x7 + x4 x6^2 x7 + x2 x3 x7^2 + 4 x2 x4 x7^2 + x3 x4 x7^2 + 4 x2 x6 x7^2 + x4 x6 x7^2 + x6^2 x7^2 + 2 x2 x7^3 + x4 x7^3, 4 + x2^4, x3 x4 + x3 x5 + x1 x6 + x3 x6 + x4 x6 + 2 x5 x6 + x6^2 + x1 x7 + x3 x7 + x5 x7 + x6 x7, x1 x4 + x1 x5 + x4 x5 + 4 x5 x6 + 4 x6^2 + 4 x5 x7 + 4 x6 x7 + 4 x7^2, x1 x3 + x1 x5 + x4 x5 + 4 x3 x6 + 3 x5 x6 + 3 x6^2 + x4 x7 + 4 x6 x7, x1 x2^2 + x2^3 + x2 x4 x5 + 4 x2 x5 x6 + x4 x5 x6 + 4 x2 x6^2 + x4 x6^2 + x2 x4 x7 + 4 x2 x6 x7 + x4 x6 x7 + x1 x7^2 + x4 x7^2 + x5 x7^2 + x7^3, x1^2 + 4 x4 x5 + x5 x6 + x6^2 + 4 x4 x7 + x6 x7}

「おおー。確かに、今度は、係数に、{0,1,2,3,4}の数字しか出てきてないな。」

「そして。F_5 の代数的閉体で考えれば、複素数の時と同じようにヒルベルトの零点定理が使えるから、今計算したようにグレブナー基底が {1} ではないことから、東京、千葉、神奈川、埼玉、山梨、静岡、長野が塗り分け可能であることが示された。」

「でも、これって、有理数の場合と比べて、特段簡単になっているわけじゃないよな？」

「同意。あまり変わらないようだ。」

「それじゃあ、意味ないってことか？」

「早計。結果の出力は、そんなに変わっていなくても、計算時間が早くなっているかもしれない。実際に、Timing で測ってみよう。」

南條は、Timing と Mathematica と打ち込んだ。

「名の通り。Timing とは、計算時間を測る関数だ。Timing の中に計算したいものを入れると、その計算にかかったCPUタイムと、出力が表示される。」

「ほほー。便利だな。」

「試しに。素因数分解をする関数 FactorInteger で練習してみよう。」

FactorInteger[931]

「えーと、これは、931を素因数分解するってことだよな？」

「適当。では、計算してみよう。」

{{7, 2}, {19, 1}}

「お、一瞬で出てきたな。323= 7^2 ×19 ってことか。」

「適切。一瞬、と言ったが、実際どのくらい計算に時間がかかるのかを、Timing で見る。」

Timing[FactorInteger[931]]

南條は、さっきの FactorInteger[931] をTiming[] で囲んだ。

Shift+Enter で実行すると、一番左に、秒数が表示された。

{0.000015, {{7, 2}, {19, 1}}}

「………0.000015って、どんだけ早いんだよ。」

「苦笑。ただ、小さ過ぎるので、精度が正しいかどうかは、分からないが、とにかくすぐ計算が終わることは分かった。」

「ああ、そうだな。」

「次に。もっと、数字を大きくしてみよう。」

18743829493847592139484200289405092382040938475738284

「うおっ。いきなりでかくなったな。」

「いざ。素因数分解。」

Timing[FactorInteger[18743829493847592139484200289405092382040938475738284]]

{9.58023, {{2, 2}, {437613735651731690521,

1}, {10707975988192351279897952558051, 1}}}

「結果。9.58023 秒……さっきよりは、時間がかかっているようだ、ね。」

「ああ。なんか出力されるまでの時間は、とてもドキドキするな…//」

「それでは。グレブナー基底の計算時間を計測してみよう。」

「……。」

Timing[GroebnerBasis[{x1^4 - 1, x2^4 - 1, x3^4 - 1, x4^4 - 1, x5^4 - 1, x6^4 - 1, x7^4 - 1, (x1 + x2)*(x1^2 + x2^2), (x1 + x3)*(x1^2 + x3^2), (x1 + x4)*(x1^2 + x4^2), (x1 + x5)*(x1^2 + x5^2), (x2 + x4)*(x1^2 + x4^2), (x4 + x5)*(x4^2 + x5^2), (x4 + x7)*(x4^2 + x7^2), (x3 + x5)*(x3^2 + x5^2), (x3 + x6)*(x3^2 + x6^2), (x5 + x6)*(x5^2 + x6^2), (x5 + x7)*(x5^2 + x7^2), (x6 + x7)*(x6^2 + x7^2)}, {x1, x2, x3, x4, x5, x6, x7}]]

「まず。標数が０、すなわち、有理数係数の場合、だ。」

「つまり、複素数での世界で、連立方程式を解くってことだな。」

{0.182451, {-1 + x7^4, x6^3 + x6^2 x7 + x6 x7^2 + x7^3, x5^2 + x5 x6 + x6^2 + x5 x7 + x6 x7 + x7^2, x4^2 + x4 x5 - x5 x6 - x6^2 + x4 x7 - x6 x7, x3 x5 x6 + x3 x6^2 + x5 x6^2 + x3 x5 x7 + x3 x6 x7 + x5 x6 x7 - x6 x7^2 - x7^3, -1 + x3 x4 x6^2 + x3 x6^2 x7 - x4 x6^2 x7 + x3 x4 x7^2 + 2 x3 x5 x7^2 + 2 x3 x6 x7^2 + 2 x5 x6 x7^2 + x6^2 x7^2 + x3 x7^3 - x4 x7^3, x3 x4 x5 + x3 x4 x6 + x4 x5 x6 - x3 x6^2 + x4 x6^2 - x3 x5 x7 - x3 x6 x7 - x5 x6 x7 - x3 x7^2 + x7^3, x3^2 + x3 x5 + x3 x6 - x5 x7 - x6 x7 - x7^2, 1 - x2^2 x3 x4 - x2^2 x3 x5 + x2^3 x6 - x2^2 x3 x6 - x2^2 x4 x6 - 2 x2^2 x5 x6 + x2 x4 x5 x6 - x2^2 x6^2 - x2 x5 x6^2 + x4 x5 x6^2 + x2^3 x7 - x2^2 x3 x7 - x2^2 x5 x7 + x2 x4 x5 x7 - x2^2 x6 x7 + x2 x4 x6 x7 - x2 x5 x6 x7 + x4 x5 x6 x7 - x2 x6^2 x7 + x4 x6^2 x7 + x2 x4 x7^2 - x3 x4 x7^2 - x3 x5 x7^2 - x3 x6 x7^2 - x5 x6 x7^2 - x6^2 x7^2 + x2 x7^3 - x3 x7^3, -1 + x2^3 x4 + x2^3 x5 - x2^2 x4 x5 + x2^2 x5 x6 - x2 x4 x5 x6 + x2^2 x6^2 - x2 x4 x6^2 + x2^2 x5 x7 - x2 x4 x5 x7 + x2^2 x6 x7 - x2 x4 x6 x7 + x2 x5 x6 x7 - x4 x5 x6 x7 + x2 x6^2 x7 - x4 x6^2 x7 + x2^2 x7^2 - x2 x4 x7^2 + x2 x6 x7^2 - x4 x6 x7^2, x2^3 x3 + x2^3 x5 - x2^2 x4 x5 + x2^2 x3 x6 - x2 x3 x4 x6 + 2 x2^2 x5 x6 - 2 x2 x4 x5 x6 + 2 x2^2 x6^2 + x2 x3 x6^2 - 2 x2 x4 x6^2 + x2 x5 x6^2 - x4 x5 x6^2 - x2^2 x4 x7 + x2 x3 x4 x7 + 2 x2 x3 x5 x7 + x2^2 x6 x7 + x2 x3 x6 x7 - x2 x4 x6 x7 + x3 x4 x6 x7 + 2 x2 x5 x6 x7 - x3 x6^2 x7 + x4 x6^2 x7 + x2 x3 x7^2 - x2 x4 x7^2 + x3 x4 x7^2 - x2 x6 x7^2 + x4 x6 x7^2 + x6^2 x7^2 - 3 x2 x7^3 + x4 x7^3, -1 + x2^4, x3 x4 + x3 x5 + x1 x6 + x3 x6 + x4 x6 + 2 x5 x6 + x6^2 + x1 x7 + x3 x7 + x5 x7 + x6 x7, x1 x4 + x1 x5 + x4 x5 - x5 x6 - x6^2 - x5 x7 - x6 x7 - x7^2, x1 x3 + x1 x5 + x4 x5 - x3 x6 - 2 x5 x6 - 2 x6^2 + x4 x7 - x6 x7, x1 x2^2 + x2^3 + x2 x4 x5 - x2 x5 x6 + x4 x5 x6 - x2 x6^2 + x4 x6^2 + x2 x4 x7 - x2 x6 x7 + x4 x6 x7 + x1 x7^2 + x4 x7^2 + x5 x7^2 + x7^3, x1^2 - x4 x5 + x5 x6 + x6^2 - x4 x7 + x6 x7}}

「出た。計算にかかった時間は、約 0.182 秒、だ。」

「ほぼ一瞬だな。」

「次に。F_5 係数でのグレブナー基底の計算時間を測定する。」

Timing[GroebnerBasis[{x1^4 + 1, x2^4 + 1, x3^4 + 1, x4^4 + 1, x5^4 + 1, x6^4 + 1, x7^4 + 1, (x1 + x2)*(x1^2 + x2^2), (x1 + x3)*(x1^2 + x3^2), (x1 + x4)*(x1^2 + x4^2), (x1 + x5)*(x1^2 + x5^2), (x2 + x4)*(x1^2 + x4^2), (x4 + x5)*(x4^2 + x5^2), (x4 + x7)*(x4^2 + x7^2), (x3 + x5)*(x3^2 + x5^2), (x3 + x6)*(x3^2 + x6^2), (x5 + x6)*(x5^2 + x6^2), (x5 + x7)*(x5^2 + x7^2), (x6 + x7)*(x6^2 + x7^2)}, {x1,x2, x3, x4, x5, x6, x7}, Modulus -> 5]]

{0.159408, {4 + x7^4, x6^3 + x6^2 x7 + x6 x7^2 + x7^3, x5^2 + x5 x6 + x6^2 + x5 x7 + x6 x7 + x7^2, x4^2 + x4 x5 + 4 x5 x6 + 4 x6^2 + x4 x7 + 4 x6 x7, x3 x5 x6 + x3 x6^2 + x5 x6^2 + x3 x5 x7 + x3 x6 x7 + x5 x6 x7 + 4 x6 x7^2 + 4 x7^3, 4 + x3 x4 x6^2 + x3 x6^2 x7 + 4 x4 x6^2 x7 + x3 x4 x7^2 + 2 x3 x5 x7^2 + 2 x3 x6 x7^2 + 2 x5 x6 x7^2 + x6^2 x7^2 + x3 x7^3 + 4 x4 x7^3, x3 x4 x5 + x3 x4 x6 + x4 x5 x6 + 4 x3 x6^2 + x4 x6^2 + 4 x3 x5 x7 + 4 x3 x6 x7 + 4 x5 x6 x7 + 4 x3 x7^2 + x7^3, x3^2 + x3 x5 + x3 x6 + 4 x5 x7 + 4 x6 x7 + 4 x7^2, 1 + 4 x2^2 x3 x4 + 4 x2^2 x3 x5 + x2^3 x6 + 4 x2^2 x3 x6 + 4 x2^2 x4 x6 + 3 x2^2 x5 x6 + x2 x4 x5 x6 + 4 x2^2 x6^2 + 4 x2 x5 x6^2 + x4 x5 x6^2 + x2^3 x7 + 4 x2^2 x3 x7 + 4 x2^2 x5 x7 + x2 x4 x5 x7 + 4 x2^2 x6 x7 + x2 x4 x6 x7 + 4 x2 x5 x6 x7 + x4 x5 x6 x7 + 4 x2 x6^2 x7 + x4 x6^2 x7 + x2 x4 x7^2 + 4 x3 x4 x7^2 + 4 x3 x5 x7^2 + 4 x3 x6 x7^2 + 4 x5 x6 x7^2 + 4 x6^2 x7^2 + x2 x7^3 + 4 x3 x7^3, 4 + x2^3 x4 + x2^3 x5 + 4 x2^2 x4 x5 + x2^2 x5 x6 + 4 x2 x4 x5 x6 + x2^2 x6^2 + 4 x2 x4 x6^2 + x2^2 x5 x7 + 4 x2 x4 x5 x7 + x2^2 x6 x7 + 4 x2 x4 x6 x7 + x2 x5 x6 x7 + 4 x4 x5 x6 x7 + x2 x6^2 x7 + 4 x4 x6^2 x7 + x2^2 x7^2 + 4 x2 x4 x7^2 + x2 x6 x7^2 + 4 x4 x6 x7^2, x2^3 x3 + x2^3 x5 + 4 x2^2 x4 x5 + x2^2 x3 x6 + 4 x2 x3 x4 x6 + 2 x2^2 x5 x6 + 3 x2 x4 x5 x6 + 2 x2^2 x6^2 + x2 x3 x6^2 + 3 x2 x4 x6^2 + x2 x5 x6^2 + 4 x4 x5 x6^2 + 4 x2^2 x4 x7 + x2 x3 x4 x7 + 2 x2 x3 x5 x7 + x2^2 x6 x7 + x2 x3 x6 x7 + 4 x2 x4 x6 x7 + x3 x4 x6 x7 + 2 x2 x5 x6 x7 + 4 x3 x6^2 x7 + x4 x6^2 x7 + x2 x3 x7^2 + 4 x2 x4 x7^2 + x3 x4 x7^2 + 4 x2 x6 x7^2 + x4 x6 x7^2 + x6^2 x7^2 + 2 x2 x7^3 + x4 x7^3, 4 + x2^4, x3 x4 + x3 x5 + x1 x6 + x3 x6 + x4 x6 + 2 x5 x6 + x6^2 + x1 x7 + x3 x7 + x5 x7 + x6 x7, x1 x4 + x1 x5 + x4 x5 + 4 x5 x6 + 4 x6^2 + 4 x5 x7 + 4 x6 x7 + 4 x7^2, x1 x3 + x1 x5 + x4 x5 + 4 x3 x6 + 3 x5 x6 + 3 x6^2 + x4 x7 + 4 x6 x7, x1 x2^2 + x2^3 + x2 x4 x5 + 4 x2 x5 x6 + x4 x5 x6 + 4 x2 x6^2 + x4 x6^2 + x2 x4 x7 + 4 x2 x6 x7 + x4 x6 x7 + x1 x7^2 + x4 x7^2 + x5 x7^2 + x7^3, x1^2 + 4 x4 x5 + x5 x6 + x6^2 + 4 x4 x7 + x6 x7}}

「出力。された。」

「今度は、えーと、0.159 秒。さっきの有理数係数の場合と比べて、わずかに早くなっているな。」

「同意。」

「やはり、係数が膨張しないことが影響しているのか？」

「不明。この実験から、分かったことは、"有理数の場合に比べ、F_5 で計算すると、わずかながら、計算時間が短くなった" ということだ。そして、その差は、0.02 秒と、わずか過ぎる。もっと、大きい連立方程式の場合に、有意な差が出るか、検証して見る必要があるだろう。」

「おおーなんか実験数学っぽいな。」

「定義。それは、実験数学の定義にもよるが、"有限体の方が早く計算が終わる"という仮説の元、実験で検証をしていくのだから、そう言ってもいいかもしれない。」

実験、言葉のイメージからは、物理とか化学で用いられる印象があるが、コンピュータを使った数学でも使われることがある。

手計算の代わりに、計算機を使って予想を証明していく様子が、それと似ているからだろう。

「具体例。差が出るかを検証するには、もっと多くの多項式が必要だ。」

「ああ。そうだな。」

「試しに。日本地図を多項式で表現してみよう。」

「マジか！？」

「疑問。なぜ？」

日本にいくつ都道府県があると思ってるんだ。４７だぞ。

１都６県でも、１７本の連立方程式だったのに、全国ってなったら、一体いくつになるんだ。

そもそも、それをすべて書くのが面倒くさい、もとい、大変だ。

「では。私は、東日本をやるから、本条は、西日本を担当してくれ。」

そう言って、南條は、多項式をずらずらと打ち込み始めた。

こういう時の南條の集中力は、凄まじいもので、もう何を言っても聞こえないだろう。

仕方ない、やるしかない。

夜更けのファミレスに、南條のキーボードの音と、俺が紙に多項式を書き出す音が響く。

こう２人で作業していると、昔、一緒に課題をやってた頃を思い出す。

南條は、顔色一つ変えずに手を動かしているが、今の俺には、その瞳の奥の情熱が、しっかりと分かる。

色々あったが、南條とは友達で良かったと思う。

「完了。作業は終了した。」

俺が、四国もまだ終わらないうちに、南條は顔を上げた。

「なんだ、もう終わったのか！？」

「YES。終了した。」

「早いな…」

「逆に。そっちは、まだ終わってない、のか？」

こちとら大層なスペックは持ち合わせてはいない。

受験の時、センター試験で９割とれたのだって、ほとんど運みたいなものだった。

「では。とりあえず、東日本だけでもグレブナー基底を計算してみよう。」

南條は、パソコンのディスプレイをこちらに向ける。

都道府県と多項式がずらっと並んでいた。

北海道 ↔︎ x_1

青森 ↔︎ x_2

岩手 ↔︎ x_3

宮城 ↔︎ x_4

秋田 ↔︎ x_5

山形 ↔︎ x_6

福島 ↔︎ x_7

茨城 ↔︎ x_8

栃木 ↔︎ x_9

群馬 ↔︎ x_10

埼玉 ↔︎ x_11

千葉 ↔︎ x_12

東京 ↔︎ x_13

神奈川 ↔︎ x_14

新潟 ↔︎ x_15

山梨 ↔︎ x_19

長野 ↔︎ x_20

静岡 ↔︎ x_22

「まず。東日本の１８の都道府県に対して、１８個の変数を対応させる。変数の添え字の数字は、総務省の都道府県コードを参考にした。x_16 など抜けている変数もあるが、それは西日本の都道府県であって、間違いではない。」

「ほほーなるほど。了解した。」

「では。次に、隣り合う関係性を表した多項式だ。」

x1^4 - 1

x2^4 - 1

x3^4 - 1

x4^4 - 1

x5^4 - 1

x6^4 - 1

x7^4 - 1

x8^4 - 1

x9^4 - 1

x10^4 - 1

x11^4 - 1

x12^4 - 1

x13^4 - 1

x14^4 - 1

x15^4 - 1

x19^4 - 1

x20^4 - 1

x22^4 - 1

(x2 + x3)*(x2^2 + x3^2)

(x2 + x5)*(x2^2 + x5^2)

(x3 + x5)*(x3^2 + x5^2)

(x3 + x4)*(x3^2 + x4^2)

(x4 + x5)*(x4^2 + x5^2)

(x4 + x6)*(x4^2 + x6^2)

(x4 + x7)*(x4^2 + x7^2)

(x5 + x6)*(x5^2 + x6^2)

(x6 + x7)*(x6^2 + x7^2)

(x6 + x15)*(x6^2 + x15^2)

(x7 + x8)*(x7^2 + x8^2)

(x7 + x9)*(x7^2 + x9^2)

(x7 + x10)*(x7^2 + x10^2)

(x7 + x15)*(x7^2 + x15^2)

(x8 + x9)*(x8^2 + x9^2)

(x8 + x11)*(x8^2 + x11^2)

(x8 + x12)*(x8^2 + x12^2)

(x9 + x10)*(x9^2 + x10^2)

(x9 + x11)*(x9^2 + x11^2)

(x10 + x11)*(x10^2 + x11^2)

(x10 + x15)*(x10^2 + x15^2)

(x10 + x20)*(x10^2 + x20^2)

(x11 + x12)*(x11^2 + x12^2)

(x11 + x13)*(x11^2 + x13^2)

(x11 + x19)*(x11^2 + x19^2)

(x11 + x20)*(x11^2 + x20^2)

(x12 + x13)*(x12^2 + x13^2)

(x13 + x14)*(x13^2 + x14^2)

(x13 + x19)*(x13^2 + x19^2)

(x14 + x19)*(x14^2 + x19^2)

(x14 + x22)*(x14^2 + x22^2)

(x15 + x20)*(x15^2 + x20^2)

(x19 + x20)*(x19^2 + x20^2)

(x19 + x22)*(x19^2 + x22^2)

(x20 + x22)*(x20^2 + x22^2)

覚悟していたことだが、めっちゃある。

手でグレブナー基底を計算しようと思ったら、気の遠くなる話だ。

「合計。53本の連立方程式、だ。それでは、早速、グレブナー基底の計算にかかる時間を計測してみよう。まずは、有理数で。」

Timing[GroebnerBasis[{x1^4 - 1, x2^4 - 1, x3^4 - 1, x4^4 - 1, x5^4 - 1, x6^4 - 1, x7^4 - 1, x8^4 - 1, x9^4 - 1, x10^4 - 1, x11^4 - 1, x12^4 - 1, x13^4 - 1, x14^4 - 1, x15^4 - 1, x19^4 - 1, x20^4 - 1, x22^4 - 1, (x2 + x3)*(x2^2 + x3^2), (x2 + x5)*(x2^2 + x5^2), (x3 + x5)*(x3^2 + x5^2), (x3 + x4)*(x3^2 + x4^2), (x4 + x5)*(x4^2 + x5^2), (x4 + x6)*(x4^2 + x6^2), (x4 + x7)*(x4^2 + x7^2), (x5 + x6)*(x5^2 + x6^2), (x6 + x7)*(x6^2 + x7^2), (x6 + x15)*(x6^2 + x15^2), (x7 + x8)*(x7^2 + x8^2), (x7 + x9)*(x7^2 + x9^2), (x7 + x10)*(x7^2 + x10^2), (x7 + x15)*(x7^2 + x15^2), (x8 + x9)*(x8^2 + x9^2), (x8 + x11)*(x8^2 + x11^2), (x8 + x12)*(x8^2 + x12^2), (x9 + x10)*(x9^2 + x10^2), (x9 + x11)*(x9^2 + x11^2), (x10 + x11)*(x10^2 + x11^2), (x10 + x15)*(x10^2 + x15^2), (x10 + x20)*(x10^2 + x20^2), (x11 + x12)*(x11^2 + x12^2), (x11 + x13)*(x11^2 + x13^2), (x11 + x19)*(x11^2 + x19^2), (x11 + x20)*(x11^2 + x20^2), (x12 + x13)*(x12^2 + x13^2), (x13 + x14)*(x13^2 + x14^2), (x13 + x19)*(x13^2 + x19^2), (x14 + x19)*(x14^2 + x19^2), (x14 + x22)*(x14^2 + x22^2), (x15 + x20)*(x15^2 + x20^2), (x19 + x20)*(x19^2 + x20^2), (x19 + x22)*(x19^2 + x22^2), (x20 + x22)*(x20^2 + x22^2)}, {x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x19, x20, x22}]]

「それでは。押す。」

「ああ……」

南條は、Shift+Enter を押した。

さあ、どうなるか。

………。

なかなか出てこない。

グレブナー基底の計算は、必ず終わることは数学で証明されているが、それがいつかは分からない。

もしかしたら、一晩中待っていても、出てこないかもしれない。

これだけ、多項式と変数があるんだから、処理が重くなっても致し方がない。

いつ終わるか分からないのを待っているのも辛いので、俺は南條に提案することにした。

「なあ、出るまで、少し休憩しないか？幸いここはファミレスだし、ドリンクバーだってたくさ」

{53.511, {-1 + x22^4, x20^3 + x20^2 x22 + x20 x22^2 + x22^3,

x19^2 + x19 x20 + x20^2 + x19 x22 + x20 x22 + x22^2,

x15^3 + x15^2 x20 + x15 x20^2 - x20^2 x22 - x20 x22^2 - x22^3,

x14^2 + x14 x19 - x19 x20 - x20^2 + x14 x22 - x20 x22,

x13^2 + x13 x14 + x13 x19 - x14 x22 - x19 x22 - x22^2,

x12^2 x14 + x12^2 x19 - x12 x14 x19 + x12^2 x20 - x12 x14 x20 -

x12 x19 x20 + x14 x19 x20 + x12^2 x22 + x12 x22^2 + x22^3,

x12^2 x13 - x12 x13 x19 - x12^2 x20 - x12 x13 x20 + x12 x19 x20 +

x13 x19 x20 + x12 x20^2 - x19 x20^2,

x12^3 - x12 x13 x14 + x13 x14 x19 + x12^2 x20 + x12 x13 x20 -

x12 x19 x20 - x13 x19 x20 - x12 x20^2 + x19 x20^2 + x12 x14 x22 +

x12 x19 x22 - x14 x19 x22 + x12 x22^2 + x22^3,

x11 x14 + x13 x14 + x11 x19 + x13 x19 + x14 x19 + x11 x20 +

x13 x20 + x14 x20 + x19 x20 + x11 x22 + x13 x22 - x22^2,

x11 x13 - x13 x14 - x11 x20 - x19 x20 - x20^2 + x14 x22 + x19 x22 +

x22^2, x11 x12 + x12^2 + x12 x13 - x11 x19 - x13 x19 + x19 x20 +

x20^2 + x19 x22 + x20 x22 + x22^2,

x11^2 + x11 x19 + x11 x20 - x19 x22 - x20 x22 - x22^2,

x10 x15^2 + x11 x15^2 + x10 x15 x19 + x11 x15 x19 + x15^2 x19 +

x10 x15 x20 + x11 x15 x20 + x15^2 x20 + x15 x19 x20 - x10 x19 x22 -

x11 x19 x22 - x15 x19 x22 - x10 x20 x22 - x11 x20 x22 -

x15 x20 x22 - x19 x20 x22 - x10 x22^2 - x11 x22^2 - x15 x22^2 +

x22^3, -2 x12 x13 x14 + 3 x12^2 x15 + x12 x13 x15 + 4 x10 x14 x15 +

x12 x14 x15 - 3 x13 x14 x15 + 3 x11 x15^2 + 3 x13 x15^2 +

3 x14 x15^2 + 2 x12^2 x19 + 4 x10 x14 x19 - 4 x13 x14 x19 -

4 x11 x15 x19 - 2 x12 x15 x19 - 4 x13 x15 x19 + 3 x15^2 x19 +

3 x12^2 x20 + x12 x13 x20 + 4 x10 x14 x20 + x12 x14 x20 -

3 x13 x14 x20 - 4 x10 x15 x20 - 2 x11 x15 x20 - 2 x12 x15 x20 +

4 x14 x15 x20 - 4 x10 x19 x20 - 8 x11 x19 x20 - 2 x12 x19 x20 -

4 x13 x19 x20 - 4 x10 x20^2 - x11 x20^2 + 3 x13 x20^2 +

3 x14 x20^2 - 4 x15 x20^2 - x19 x20^2 - x12 x13 x22 +

4 x10 x14 x22 + 2 x12 x14 x22 - 2 x13 x14 x22 + x12 x15 x22 -

x13 x15 x22 + 3 x14 x15 x22 - x15^2 x22 - x11 x19 x22 +

2 x12 x19 x22 - x13 x19 x22 + 3 x15 x19 x22 - 4 x10 x20 x22 -

4 x11 x20 x22 + x12 x20 x22 - x13 x20 x22 + 3 x14 x20 x22 -

2 x15 x20 x22 + x12 x13 x14 x15^2 x20 x22 + 3 x19 x20 x22 -

x12^2 x15^2 x19 x20 x22 - x20^2 x22 + x12 x13 x14 x15 x20^2 x22 -

2 x12^2 x15^2 x20^2 x22 - x12 x13 x15^2 x20^2 x22 -

x12^2 x15 x19 x20^2 x22 + x11 x15^2 x19 x20^2 x22 +

2 x12 x15^2 x19 x20^2 x22 + x13 x15^2 x19 x20^2 x22 + x11 x22^2 +

3 x12 x22^2 + 2 x13 x22^2 + 2 x14 x22^2 + 2 x15 x22^2 -

x12 x13 x14 x15^2 x22^2 + 2 x19 x22^2 + x12^2 x15^2 x19 x22^2 +

6 x20 x22^2 + x12^2 x15^2 x20 x22^2 + x12 x13 x15^2 x20 x22^2 -

x12 x14 x15^2 x20 x22^2 - x13 x14 x15^2 x20 x22^2 -

2 x11 x15^2 x19 x20 x22^2 - 2 x12 x15^2 x19 x20 x22^2 -

2 x13 x15^2 x19 x20 x22^2 - x12 x13 x14 x20^2 x22^2 +

x12^2 x15 x20^2 x22^2 + x12 x13 x15 x20^2 x22^2 -

x12 x14 x15 x20^2 x22^2 - x13 x14 x15 x20^2 x22^2 -

x11 x15^2 x20^2 x22^2 - x12 x15^2 x20^2 x22^2 +

x12^2 x19 x20^2 x22^2 - 2 x11 x15 x19 x20^2 x22^2 -

2 x12 x15 x19 x20^2 x22^2 - 2 x13 x15 x19 x20^2 x22^2 - x22^3 -

x12 x13 x14 x15 x22^3 + x12^2 x15^2 x22^3 + x12 x14 x15^2 x22^3 +

x13 x14 x15^2 x22^3 + x12^2 x15 x19 x22^3 + x11 x15^2 x19 x22^3 +

x13 x15^2 x19 x22^3 - x12 x13 x14 x20 x22^3 +

4 x12^2 x15 x20 x22^3 + 2 x12 x13 x15 x20 x22^3 +

2 x11 x15^2 x20 x22^3 - 3 x12 x15^2 x20 x22^3 +

x13 x15^2 x20 x22^3 + x14 x15^2 x20 x22^3 + x12^2 x19 x20 x22^3 -

2 x11 x15 x19 x20 x22^3 - 4 x12 x15 x19 x20 x22^3 -

2 x13 x15 x19 x20 x22^3 + 5 x15^2 x19 x20 x22^3 +

x12^2 x20^2 x22^3 + x12 x14 x20^2 x22^3 + x13 x14 x20^2 x22^3 +

2 x11 x15 x20^2 x22^3 - 3 x12 x15 x20^2 x22^3 +

x13 x15 x20^2 x22^3 + x14 x15 x20^2 x22^3 + x15^2 x20^2 x22^3 +

x11 x19 x20^2 x22^3 + x13 x19 x20^2 x22^3 + 5 x15 x19 x20^2 x22^3,

4 x10 x13 + x12 x13 - x12 x14 + 2 x13 x14 + 4 x10 x15 - x12 x15 +

x13 x15 - x14 x15 + 6 x15^2 + 4 x10 x19 + 2 x11 x19 - x13 x19 -

x14 x19 - x15 x19 - x12 x13 x14 x15^2 x19 + 4 x10 x20 +

5 x11 x20 + 3 x13 x20 + 5 x15 x20 - 2 x12 x13 x14 x15^2 x20 +

6 x19 x20 + x12 x13 x14 x15 x19 x20 + x12^2 x15^2 x19 x20 +

x12 x13 x15^2 x19 x20 - 2 x13 x14 x15^2 x19 x20 + 8 x20^2 -

x12 x13 x14 x15 x20^2 + 2 x12^2 x15^2 x20^2 +

2 x12 x13 x15^2 x20^2 - x13 x14 x15^2 x20^2 - x12^2 x15 x19 x20^2 -

x12 x13 x15 x19 x20^2 - x13 x14 x15 x19 x20^2 -

3 x11 x15^2 x19 x20^2 - 2 x12 x15^2 x19 x20^2 -

x13 x15^2 x19 x20^2 - x12 x22 - 2 x14 x22 - x15 x22 - 3 x19 x22 -

x12^2 x15^2 x19 x22 + x12 x14 x15^2 x19 x22 -

x12^2 x15^2 x20 x22 + 2 x12 x14 x15^2 x20 x22 +

x12^2 x15 x19 x20 x22 - x12 x14 x15 x19 x20 x22 +

3 x11 x15^2 x19 x20 x22 + x12 x15^2 x19 x20 x22 +

3 x13 x15^2 x19 x20 x22 + 2 x14 x15^2 x19 x20 x22 +

x12 x13 x14 x20^2 x22 - x12^2 x15 x20^2 x22 -

x12 x13 x15 x20^2 x22 + x12 x14 x15 x20^2 x22 +

x13 x14 x15 x20^2 x22 + x11 x15^2 x20^2 x22 + x14 x15^2 x20^2 x22 +

x13 x14 x19 x20^2 x22 + 4 x11 x15 x19 x20^2 x22 +

x12 x15 x19 x20^2 x22 + 3 x13 x15 x19 x20^2 x22 +

x14 x15 x19 x20^2 x22 - 2 x22^2 - x12^2 x15^2 x22^2 +

x12 x13 x14 x20 x22^2 - x12^2 x15 x20 x22^2 -

x12 x13 x15 x20 x22^2 + x13 x14 x15 x20 x22^2 +

x11 x15^2 x20 x22^2 + 2 x12 x15^2 x20 x22^2 +

x13 x14 x19 x20 x22^2 + 4 x11 x15 x19 x20 x22^2 +

2 x12 x15 x19 x20 x22^2 + 3 x13 x15 x19 x20 x22^2 -

3 x15^2 x19 x20 x22^2 - x12 x14 x20^2 x22^2 + x12 x15 x20^2 x22^2 -

x14 x15 x20^2 x22^2 + x15^2 x20^2 x22^2 - x11 x19 x20^2 x22^2 -

x13 x19 x20^2 x22^2 - x14 x19 x20^2 x22^2 - 4 x15 x19 x20^2 x22^2 +

x12 x13 x14 x22^3 - 2 x12^2 x15 x22^3 - x12 x13 x15 x22^3 +

x13 x14 x15 x22^3 - 2 x11 x15^2 x22^3 - 3 x13 x15^2 x22^3 +

x13 x14 x19 x22^3 + 4 x11 x15 x19 x22^3 + 2 x12 x15 x19 x22^3 +

3 x13 x15 x19 x22^3 - 3 x15^2 x19 x22^3 - x12 x14 x20 x22^3 +

3 x12 x15 x20 x22^3 - x14 x15 x20 x22^3 - 4 x15^2 x20 x22^3 -

x11 x19 x20 x22^3 - x13 x19 x20 x22^3 - x14 x19 x20 x22^3 -

4 x15 x19 x20 x22^3 - x11 x20^2 x22^3 - x13 x20^2 x22^3 -

5 x15 x20^2 x22^3,

4 x10 x12 - 2 x12^2 - 3 x12 x13 + x12 x14 + 2 x12 x15 - x13 x15 -

x14 x15 + 3 x15^2 + 4 x11 x19 + 3 x13 x19 - x14 x19 + 4 x15 x19 +

x12 x13 x14 x15^2 x19 - 4 x10 x20 - 2 x11 x20 + 3 x12 x20 +

2 x15 x20 + 2 x12 x13 x14 x15^2 x20 - 3 x19 x20 -

x12 x13 x14 x15 x19 x20 + 2 x12^2 x15^2 x19 x20 +

2 x12 x13 x15^2 x19 x20 - x13 x14 x15^2 x19 x20 - 6 x20^2 +

x12 x13 x14 x15 x20^2 - 2 x12^2 x15^2 x20^2 -

2 x12 x13 x15^2 x20^2 + x13 x14 x15^2 x20^2 +

4 x12^2 x15 x19 x20^2 + 4 x12 x13 x15 x19 x20^2 -

2 x13 x14 x15 x19 x20^2 + 6 x11 x15^2 x19 x20^2 +

2 x12 x15^2 x19 x20^2 + 4 x13 x15^2 x19 x20^2 + x12 x22 -

6 x19 x22 - x12 x13 x15^2 x19 x22 - x12 x14 x15^2 x19 x22 +

x13 x14 x15^2 x19 x22 - 5 x20 x22 - x12 x13 x15^2 x20 x22 -

2 x12 x14 x15^2 x20 x22 + x13 x14 x15^2 x20 x22 +

x12 x13 x15 x19 x20 x22 + x12 x14 x15 x19 x20 x22 -

x13 x14 x15 x19 x20 x22 + 2 x11 x15^2 x19 x20 x22 +

x12 x15^2 x19 x20 x22 + 2 x13 x15^2 x19 x20 x22 +

x14 x15^2 x19 x20 x22 - x12 x13 x14 x20^2 x22 -

x12 x14 x15 x20^2 x22 - 2 x11 x15^2 x20^2 x22 -

x13 x15^2 x20^2 x22 - x14 x15^2 x20^2 x22 -

2 x12^2 x19 x20^2 x22 - 2 x12 x13 x19 x20^2 x22 +

x13 x14 x19 x20^2 x22 + x12 x15 x19 x20^2 x22 +

x13 x15 x19 x20^2 x22 + 2 x14 x15 x19 x20^2 x22 -

5 x15^2 x19 x20^2 x22 - 5 x22^2 - x12 x13 x15^2 x22^2 +

x13 x14 x15^2 x22^2 - x14 x15^2 x19 x22^2 -

x12 x13 x14 x20 x22^2 - 2 x11 x15^2 x20 x22^2 -

2 x12 x15^2 x20 x22^2 - x13 x15^2 x20 x22^2 -

x14 x15^2 x20 x22^2 - 2 x12^2 x19 x20 x22^2 -

2 x12 x13 x19 x20 x22^2 + x13 x14 x19 x20 x22^2 -

4 x11 x15 x19 x20 x22^2 - x12 x15 x19 x20 x22^2 -

3 x13 x15 x19 x20 x22^2 + x14 x15 x19 x20 x22^2 +

x15^2 x19 x20 x22^2 + x12 x14 x20^2 x22^2 - x12 x15 x20^2 x22^2 -

2 x11 x19 x20^2 x22^2 - x12 x19 x20^2 x22^2 -

2 x13 x19 x20^2 x22^2 - x14 x19 x20^2 x22^2 +

4 x15 x19 x20^2 x22^2 - x12 x13 x14 x22^3 - x12 x13 x15 x22^3 +

x13 x14 x15 x22^3 - 4 x11 x15^2 x22^3 - 2 x12 x15^2 x22^3 -

3 x13 x15^2 x22^3 - x14 x15^2 x22^3 - 2 x12^2 x19 x22^3 -

2 x12 x13 x19 x22^3 + x13 x14 x19 x22^3 - 4 x11 x15 x19 x22^3 -

x12 x15 x19 x22^3 - 3 x13 x15 x19 x22^3 + x12 x14 x20 x22^3 -

4 x11 x15 x20 x22^3 - 4 x12 x15 x20 x22^3 - 4 x13 x15 x20 x22^3 +

4 x15^2 x20 x22^3 - 2 x11 x19 x20 x22^3 - x12 x19 x20 x22^3 -

2 x13 x19 x20 x22^3 - x14 x19 x20 x22^3 + 5 x15 x19 x20 x22^3 -

2 x11 x20^2 x22^3 - x12 x20^2 x22^3 - 2 x13 x20^2 x22^3 +

3 x15 x20^2 x22^3,

x10 x11 - x10 x15 - x15^2 - x11 x19 - x15 x20 + x19 x22 + x20 x22 +

x22^2, x10^2 + x10 x15 + x15^2 + x10 x20 + x15 x20 +

x20^2, -x10 x20 - x11 x20 - x20^2 + x10 x9 + x11 x9 + x9^2,

4 + 5 x12 x13 x14 x15 - x12 x13 x15^2 - 4 x13 x14 x15^2 +

2 x12 x13 x14 x19 - 4 x12^2 x15 x19 - 3 x12 x13 x15 x19 -

3 x12 x14 x15 x19 + x13 x14 x15 x19 - 4 x11 x15^2 x19 -

12 x13 x15^2 x19 - 5 x14 x15^2 x19 + x12 x13 x14 x20 -

4 x12^2 x15 x20 - 4 x12 x13 x15 x20 - 2 x12 x14 x15 x20 -

2 x13 x14 x15 x20 - 8 x11 x15^2 x20 - 3 x12 x15^2 x20 -

7 x13 x15^2 x20 - 3 x14 x15^2 x20 + x12 x13 x19 x20 -

4 x10 x14 x19 x20 - 3 x12 x14 x19 x20 + x13 x14 x19 x20 +

4 x10 x15 x19 x20 - 4 x11 x15 x19 x20 + 2 x12 x15 x19 x20 -

10 x13 x15 x19 x20 - 8 x14 x15 x19 x20 + 9 x15^2 x19 x20 -

x12 x13 x20^2 + 4 x10 x14 x20^2 - 4 x13 x14 x20^2 -

4 x10 x15 x20^2 - 8 x11 x15 x20^2 + x12 x15 x20^2 -

11 x13 x15 x20^2 - 3 x14 x15 x20^2 + 2 x15^2 x20^2 +

4 x10 x19 x20^2 - 4 x13 x19 x20^2 - 5 x14 x19 x20^2 +

5 x15 x19 x20^2 - x12 x13 x14 x22 + 4 x12^2 x15 x22 +

x12 x13 x15 x22 - 5 x12 x14 x15 x22 - x13 x14 x15 x22 +

8 x11 x15^2 x22 + 5 x12 x15^2 x22 + x13 x15^2 x22 -

4 x14 x15^2 x22 + 3 x12 x13 x19 x22 - 12 x10 x14 x19 x22 -

2 x12 x14 x19 x22 + 6 x13 x14 x19 x22 + 12 x10 x15 x19 x22 -

5 x12 x15 x19 x22 - x13 x15 x19 x22 - 5 x14 x15 x19 x22 +

12 x15^2 x19 x22 + x12 x13 x20 x22 - 4 x10 x14 x20 x22 -

x12 x14 x20 x22 + 3 x13 x14 x20 x22 + 4 x10 x15 x20 x22 +

4 x11 x15 x20 x22 - 4 x13 x15 x20 x22 - 6 x14 x15 x20 x22 +

11 x15^2 x20 x22 + 8 x10 x19 x20 x22 + 8 x11 x19 x20 x22 -

x12 x19 x20 x22 + 7 x13 x19 x20 x22 - 5 x14 x19 x20 x22 +

10 x15 x19 x20 x22 - 3 x12 x13 x14 x15^2 x19 x20 x22 +

12 x10 x20^2 x22 + 4 x11 x20^2 x22 + x12 x20^2 x22 +

x13 x20^2 x22 - 4 x14 x20^2 x22 + 15 x15 x20^2 x22 -

x12 x13 x14 x15^2 x20^2 x22 + 4 x19 x20^2 x22 -

3 x12 x13 x14 x15 x19 x20^2 x22 + 4 x12^2 x15^2 x19 x20^2 x22 +

3 x12 x13 x15^2 x19 x20^2 x22 + x12 x14 x22^2 + x13 x14 x22^2 +

4 x11 x15 x22^2 + 3 x12 x15 x22^2 + 3 x13 x15 x22^2 +

x14 x15 x22^2 - 9 x15^2 x22^2 - 12 x10 x19 x22^2 -

8 x11 x19 x22^2 - 3 x12 x19 x22^2 + x13 x19 x22^2 -

6 x14 x19 x22^2 - 7 x15 x19 x22^2 +

3 x12 x13 x14 x15^2 x19 x22^2 - 4 x11 x20 x22^2 - x12 x20 x22^2 +

3 x13 x20 x22^2 - 3 x14 x20 x22^2 - 8 x15 x20 x22^2 +

x12 x13 x14 x15^2 x20 x22^2 - 15 x19 x20 x22^2 -

4 x12^2 x15^2 x19 x20 x22^2 - 3 x12 x13 x15^2 x19 x20 x22^2 +

3 x12 x14 x15^2 x19 x20 x22^2 + 3 x13 x14 x15^2 x19 x20 x22^2 -

5 x20^2 x22^2 + x12 x13 x14 x15 x20^2 x22^2 -

2 x12 x13 x15^2 x20^2 x22^2 + x12 x14 x15^2 x20^2 x22^2 +

x13 x14 x15^2 x20^2 x22^2 + 3 x12 x13 x14 x19 x20^2 x22^2 -

4 x12^2 x15 x19 x20^2 x22^2 - 3 x12 x13 x15 x19 x20^2 x22^2 +

3 x12 x14 x15 x19 x20^2 x22^2 + 3 x13 x14 x15 x19 x20^2 x22^2 +

x12 x15^2 x19 x20^2 x22^2 - 3 x13 x15^2 x19 x20^2 x22^2 +

4 x10 x22^3 + 4 x13 x22^3 - x14 x22^3 + x15 x22^3 - x19 x22^3 +

3 x12 x13 x14 x15 x19 x22^3 - 3 x12 x14 x15^2 x19 x22^3 -

3 x13 x14 x15^2 x19 x22^3 - 3 x20 x22^3 +

2 x12 x13 x14 x15 x20 x22^3 - x12 x13 x15^2 x20 x22^3 -

x12 x14 x15^2 x20 x22^3 - x13 x14 x15^2 x20 x22^3 +

3 x12 x13 x14 x19 x20 x22^3 - 8 x12^2 x15 x19 x20 x22^3 -

6 x12 x13 x15 x19 x20 x22^3 - 12 x11 x15^2 x19 x20 x22^3 -

x12 x15^2 x19 x20 x22^3 - 9 x13 x15^2 x19 x20 x22^3 -

3 x14 x15^2 x19 x20 x22^3 - x12 x13 x15 x20^2 x22^3 -

x12 x14 x15 x20^2 x22^3 - x13 x14 x15 x20^2 x22^3 +

2 x12 x15^2 x20^2 x22^3 + 2 x13 x15^2 x20^2 x22^3 -

x14 x15^2 x20^2 x22^3 - 3 x12 x14 x19 x20^2 x22^3 -

3 x13 x14 x19 x20^2 x22^3 - 12 x11 x15 x19 x20^2 x22^3 -

x12 x15 x19 x20^2 x22^3 - 9 x13 x15 x19 x20^2 x22^3 -

3 x14 x15 x19 x20^2 x22^3 + 7 x15^2 x19 x20^2 x22^3 +

4 x13 x15^2 x8 + 4 x14 x15^2 x8 - 4 x13 x15 x19 x8 -

4 x14 x15 x19 x8 + 4 x15^2 x19 x8 + 4 x15 x19 x20 x8 +

4 x15 x20^2 x8 - 4 x13 x15 x22 x8 - 4 x14 x15 x22 x8 +

4 x15^2 x22 x8 + 4 x13 x19 x22 x8 + 4 x14 x19 x22 x8 -

4 x15 x19 x22 x8 + 4 x15 x20 x22 x8 - 4 x19 x20 x22 x8 -

4 x20^2 x22 x8 - 4 x20 x22^2 x8 - 4 x22^3 x8,

4 - x12 x13 x14 x15 - 4 x12^2 x15^2 + x12 x13 x15^2 +

8 x13 x14 x15^2 - 6 x12 x13 x14 x19 + 4 x12^2 x15 x19 +

3 x12 x13 x15 x19 + 3 x12 x14 x15 x19 - 5 x13 x14 x15 x19 +

8 x11 x15^2 x19 + 4 x12 x15^2 x19 + 16 x13 x15^2 x19 +

5 x14 x15^2 x19 - x12 x13 x14 x20 - 4 x12^2 x15 x20 +

2 x12 x14 x15 x20 + 6 x13 x14 x15 x20 + 4 x11 x15^2 x20 +

7 x12 x15^2 x20 + 11 x13 x15^2 x20 + 3 x14 x15^2 x20 +

4 x12^2 x19 x20 + 3 x12 x13 x19 x20 + 4 x10 x14 x19 x20 +

3 x12 x14 x19 x20 - 5 x13 x14 x19 x20 - 16 x10 x15 x19 x20 +

4 x11 x15 x19 x20 + 6 x12 x15 x19 x20 + 18 x13 x15 x19 x20 +

8 x14 x15 x19 x20 - 21 x15^2 x19 x20 - 4 x12^2 x20^2 +

x12 x13 x20^2 - 4 x10 x14 x20^2 + 4 x13 x14 x20^2 +

4 x10 x15 x20^2 + 8 x11 x15 x20^2 + 7 x12 x15 x20^2 +

15 x13 x15 x20^2 + 3 x14 x15 x20^2 - 6 x15^2 x20^2 +

12 x11 x19 x20^2 + 4 x12 x19 x20^2 + 12 x13 x19 x20^2 +

5 x14 x19 x20^2 - 17 x15 x19 x20^2 + x12 x13 x14 x22 -

4 x12^2 x15 x22 - x12 x13 x15 x22 + x12 x14 x15 x22 +

x13 x14 x15 x22 - 8 x11 x15^2 x22 - 5 x12 x15^2 x22 -

x13 x15^2 x22 - 4 x12^2 x19 x22 - 3 x12 x13 x19 x22 +

12 x10 x14 x19 x22 + 6 x12 x14 x19 x22 - 6 x13 x14 x19 x22 +

8 x11 x15 x19 x22 + 5 x12 x15 x19 x22 + 5 x13 x15 x19 x22 +

9 x14 x15 x19 x22 - 12 x15^2 x19 x22 - 4 x12^2 x20 x22 -

x12 x13 x20 x22 + 4 x10 x14 x20 x22 + x12 x14 x20 x22 -

3 x13 x14 x20 x22 + 8 x10 x15 x20 x22 + 4 x11 x15 x20 x22 +

4 x12 x15 x20 x22 + 8 x13 x15 x20 x22 + 2 x14 x15 x20 x22 -

7 x15^2 x20 x22 + 12 x10 x19 x20 x22 + 16 x11 x19 x20 x22 +

5 x12 x19 x20 x22 + x13 x19 x20 x22 + 9 x14 x19 x20 x22 -

2 x15 x19 x20 x22 + 3 x12 x13 x14 x15^2 x19 x20 x22 -

5 x12 x20^2 x22 - x13 x20^2 x22 + 4 x14 x20^2 x22 -

7 x15 x20^2 x22 + x12 x13 x14 x15^2 x20^2 x22 - 4 x19 x20^2 x22 +

3 x12 x13 x14 x15 x19 x20^2 x22 - 4 x12^2 x15^2 x19 x20^2 x22 -

3 x12 x13 x15^2 x19 x20^2 x22 - 4 x12^2 x22^2 - x12 x14 x22^2 -

x13 x14 x22^2 + 12 x10 x15 x22^2 + 4 x11 x15 x22^2 -

3 x12 x15 x22^2 + x13 x15 x22^2 - x14 x15 x22^2 + 9 x15^2 x22^2 +

12 x10 x19 x22^2 + 8 x11 x19 x22^2 + 3 x12 x19 x22^2 -

x13 x19 x22^2 + 6 x14 x19 x22^2 + 7 x15 x19 x22^2 -

3 x12 x13 x14 x15^2 x19 x22^2 + 12 x10 x20 x22^2 +

8 x11 x20 x22^2 - 3 x12 x20 x22^2 - 3 x13 x20 x22^2 +

3 x14 x20 x22^2 + 12 x15 x20 x22^2 - x12 x13 x14 x15^2 x20 x22^2 +

7 x19 x20 x22^2 + 4 x12^2 x15^2 x19 x20 x22^2 +

3 x12 x13 x15^2 x19 x20 x22^2 - 3 x12 x14 x15^2 x19 x20 x22^2 -

3 x13 x14 x15^2 x19 x20 x22^2 + 5 x20^2 x22^2 -

x12 x13 x14 x15 x20^2 x22^2 + 2 x12 x13 x15^2 x20^2 x22^2 -

x12 x14 x15^2 x20^2 x22^2 - x13 x14 x15^2 x20^2 x22^2 -

3 x12 x13 x14 x19 x20^2 x22^2 + 4 x12^2 x15 x19 x20^2 x22^2 +

3 x12 x13 x15 x19 x20^2 x22^2 - 3 x12 x14 x15 x19 x20^2 x22^2 -

3 x13 x14 x15 x19 x20^2 x22^2 - x12 x15^2 x19 x20^2 x22^2 +

3 x13 x15^2 x19 x20^2 x22^2 - 12 x10 x22^3 - 20 x11 x22^3 -

12 x12 x22^3 - 12 x13 x22^3 + x14 x22^3 - 9 x15 x22^3 -

7 x19 x22^3 - 3 x12 x13 x14 x15 x19 x22^3 +

3 x12 x14 x15^2 x19 x22^3 + 3 x13 x14 x15^2 x19 x22^3 -

9 x20 x22^3 - 2 x12 x13 x14 x15 x20 x22^3 +

x12 x13 x15^2 x20 x22^3 + x12 x14 x15^2 x20 x22^3 +

x13 x14 x15^2 x20 x22^3 - 3 x12 x13 x14 x19 x20 x22^3 +

8 x12^2 x15 x19 x20 x22^3 + 6 x12 x13 x15 x19 x20 x22^3 +

12 x11 x15^2 x19 x20 x22^3 + x12 x15^2 x19 x20 x22^3 +

9 x13 x15^2 x19 x20 x22^3 + 3 x14 x15^2 x19 x20 x22^3 +

x12 x13 x15 x20^2 x22^3 + x12 x14 x15 x20^2 x22^3 +

x13 x14 x15 x20^2 x22^3 - 2 x12 x15^2 x20^2 x22^3 -

2 x13 x15^2 x20^2 x22^3 + x14 x15^2 x20^2 x22^3 +

3 x12 x14 x19 x20^2 x22^3 + 3 x13 x14 x19 x20^2 x22^3 +

12 x11 x15 x19 x20^2 x22^3 + x12 x15 x19 x20^2 x22^3 +

9 x13 x15 x19 x20^2 x22^3 + 3 x14 x15 x19 x20^2 x22^3 -

7 x15^2 x19 x20^2 x22^3 + 4 x13 x14 x15 x8 - 4 x14 x15^2 x8 -

4 x13 x14 x19 x8 + 4 x13 x15 x19 x8 + 4 x14 x15 x19 x8 -

4 x15^2 x19 x8 + 4 x13 x15 x20 x8 - 4 x15^2 x20 x8 +

4 x13 x20^2 x8 - 4 x15 x20^2 x8 + 4 x13 x15 x22 x8 -

4 x15^2 x22 x8 + 4 x13 x20 x22 x8 - 4 x15 x20 x22 x8 +

4 x13 x22^2 x8 - 4 x15 x22^2 x8, -5 x12^2 x15 - 5 x12 x13 x15 +

5 x13 x14 x15 - 9 x11 x15^2 - x13 x15^2 + 2 x12^2 x19 +

2 x12 x13 x19 - 2 x13 x14 x19 - 12 x10 x15 x19 + 8 x11 x15 x19 +

6 x12 x15 x19 + 12 x13 x15 x19 + 3 x14 x15 x19 - 17 x15^2 x19 -

2 x12^2 x20 - 2 x12 x13 x20 + 2 x13 x14 x20 - 4 x10 x15 x20 -

4 x11 x15 x20 + 3 x12 x15 x20 + 4 x13 x15 x20 + x14 x15 x20 -

12 x15^2 x20 + 11 x11 x19 x20 + 3 x12 x19 x20 + 7 x13 x19 x20 -

15 x15 x19 x20 + 4 x10 x20^2 + 10 x11 x20^2 + 4 x12 x20^2 +

6 x13 x20^2 - 13 x15 x20^2 + x19 x20^2 - 3 x12^2 x15^2 x19 x20^2 -

3 x12 x13 x15^2 x19 x20^2 + 3 x13 x14 x15^2 x19 x20^2 -

5 x14 x15 x22 + x15^2 x22 + 12 x10 x19 x22 + 17 x11 x19 x22 +

3 x12 x19 x22 + 5 x13 x19 x22 + 2 x14 x19 x22 - 4 x15 x19 x22 +

12 x10 x20 x22 + 17 x11 x20 x22 + 3 x12 x20 x22 + 5 x13 x20 x22 -

2 x14 x20 x22 - x15 x20 x22 + x19 x20 x22 +

x12^2 x15^2 x19 x20 x22 + x12 x13 x15^2 x19 x20 x22 -

x13 x14 x15^2 x19 x20 x22 - 5 x20^2 x22 + x12^2 x15^2 x20^2 x22 +

x12 x13 x15^2 x20^2 x22 - x13 x14 x15^2 x20^2 x22 +

2 x12^2 x15 x19 x20^2 x22 + 2 x12 x13 x15 x19 x20^2 x22 -

2 x13 x14 x15 x19 x20^2 x22 - 2 x11 x15^2 x19 x20^2 x22 -

2 x12 x15^2 x19 x20^2 x22 - 2 x13 x15^2 x19 x20^2 x22 -

3 x14 x15^2 x19 x20^2 x22 + 12 x10 x22^2 + 17 x11 x22^2 +

3 x12 x22^2 + 5 x13 x22^2 - 6 x15 x22^2 - 7 x20 x22^2 +

x12^2 x15^2 x20 x22^2 + x12 x13 x15^2 x20 x22^2 -

x13 x14 x15^2 x20 x22^2 + 3 x12^2 x15 x19 x20 x22^2 +

3 x12 x13 x15 x19 x20 x22^2 - 3 x13 x14 x15 x19 x20 x22^2 +

3 x11 x15^2 x19 x20 x22^2 + 3 x13 x15^2 x19 x20 x22^2 +

x14 x15^2 x19 x20 x22^2 + x14 x15^2 x20^2 x22^2 +

4 x11 x15 x19 x20^2 x22^2 + x12 x15 x19 x20^2 x22^2 +

4 x13 x15 x19 x20^2 x22^2 + 2 x14 x15 x19 x20^2 x22^2 -

3 x15^2 x19 x20^2 x22^2 - 10 x22^3 + 3 x12^2 x15 x19 x22^3 +

3 x12 x13 x15 x19 x22^3 - 3 x13 x14 x15 x19 x22^3 +

3 x11 x15^2 x19 x22^3 + 3 x13 x15^2 x19 x22^3 +

x12^2 x15 x20 x22^3 + x12 x13 x15 x20 x22^3 -

x13 x14 x15 x20 x22^3 + 5 x11 x15^2 x20 x22^3 +

2 x12 x15^2 x20 x22^3 + 5 x13 x15^2 x20 x22^3 +

x14 x15^2 x20 x22^3 + 4 x11 x15 x19 x20 x22^3 +

x12 x15 x19 x20 x22^3 + 4 x13 x15 x19 x20 x22^3 +

3 x14 x15 x19 x20 x22^3 - 2 x15^2 x19 x20 x22^3 +

4 x11 x15 x20^2 x22^3 + x12 x15 x20^2 x22^3 +

4 x13 x15 x20^2 x22^3 + x15^2 x20^2 x22^3 - x15 x19 x20^2 x22^3 +

4 x12 x15 x8 + 4 x13 x15 x8 - 4 x15^2 x8 - 4 x12 x19 x8 -

4 x13 x19 x8 + 4 x15 x19 x8 - 4 x15 x20 x8 + 4 x19 x20 x8 +

2 x12^2 x9 + 2 x12 x13 x9 - 2 x13 x14 x9 + x12 x15 x9 -

2 x14 x15 x9 + 5 x15^2 x9 - 6 x11 x19 x9 - 4 x12 x19 x9 -

6 x13 x19 x9 - 2 x14 x19 x9 + 3 x15 x19 x9 - x11 x20 x9 -

x12 x20 x9 - x13 x20 x9 + 3 x15 x20 x9 + 3 x19 x20 x9 +

3 x12^2 x15^2 x19 x20 x9 + 3 x12 x13 x15^2 x19 x20 x9 -

3 x13 x14 x15^2 x19 x20 x9 + 6 x20^2 x9 +

3 x12^2 x15 x19 x20^2 x9 + 3 x12 x13 x15 x19 x20^2 x9 -

3 x13 x14 x15 x19 x20^2 x9 + 3 x11 x15^2 x19 x20^2 x9 +

3 x13 x15^2 x19 x20^2 x9 + 2 x14 x22 x9 - x15 x22 x9 +

3 x19 x22 x9 - x12^2 x15^2 x19 x22 x9 - x12 x13 x15^2 x19 x22 x9 +

x13 x14 x15^2 x19 x22 x9 + 3 x20 x22 x9 - x12^2 x15^2 x20 x22 x9 -

x12 x13 x15^2 x20 x22 x9 + x13 x14 x15^2 x20 x22 x9 +

x12^2 x15 x19 x20 x22 x9 + x12 x13 x15 x19 x20 x22 x9 -

x13 x14 x15 x19 x20 x22 x9 + 5 x11 x15^2 x19 x20 x22 x9 +

2 x12 x15^2 x19 x20 x22 x9 + 5 x13 x15^2 x19 x20 x22 x9 +

3 x14 x15^2 x19 x20 x22 x9 - x12^2 x15 x20^2 x22 x9 -

x12 x13 x15 x20^2 x22 x9 + x13 x14 x15 x20^2 x22 x9 -

x11 x15^2 x20^2 x22 x9 - x13 x15^2 x20^2 x22 x9 -

2 x12^2 x19 x20^2 x22 x9 - 2 x12 x13 x19 x20^2 x22 x9 +

2 x13 x14 x19 x20^2 x22 x9 + 4 x11 x15 x19 x20^2 x22 x9 +

2 x12 x15 x19 x20^2 x22 x9 + 4 x13 x15 x19 x20^2 x22 x9 +

3 x14 x15 x19 x20^2 x22 x9 - 5 x15^2 x19 x20^2 x22 x9 +

5 x22^2 x9 - x12^2 x15^2 x22^2 x9 - x12 x13 x15^2 x22^2 x9 +

x13 x14 x15^2 x22^2 x9 - x14 x15^2 x19 x22^2 x9 -

x12^2 x15 x20 x22^2 x9 - x12 x13 x15 x20 x22^2 x9 +

x13 x14 x15 x20 x22^2 x9 - x11 x15^2 x20 x22^2 x9 -

x13 x15^2 x20 x22^2 x9 - x14 x15^2 x20 x22^2 x9 -

2 x12^2 x19 x20 x22^2 x9 - 2 x12 x13 x19 x20 x22^2 x9 +

2 x13 x14 x19 x20 x22^2 x9 + x12 x15 x19 x20 x22^2 x9 +

x14 x15 x19 x20 x22^2 x9 - 2 x15^2 x19 x20 x22^2 x9 -

x14 x15 x20^2 x22^2 x9 + x15^2 x20^2 x22^2 x9 -

3 x11 x19 x20^2 x22^2 x9 - x12 x19 x20^2 x22^2 x9 -

3 x13 x19 x20^2 x22^2 x9 - 2 x14 x19 x20^2 x22^2 x9 -

2 x12^2 x15 x22^3 x9 - 2 x12 x13 x15 x22^3 x9 +

2 x13 x14 x15 x22^3 x9 - 6 x11 x15^2 x22^3 x9 -

2 x12 x15^2 x22^3 x9 - 6 x13 x15^2 x22^3 x9 - x14 x15^2 x22^3 x9 -

2 x12^2 x19 x22^3 x9 - 2 x12 x13 x19 x22^3 x9 +

2 x13 x14 x19 x22^3 x9 + x12 x15 x19 x22^3 x9 -

3 x15^2 x19 x22^3 x9 - 4 x11 x15 x20 x22^3 x9 -

x12 x15 x20 x22^3 x9 - 4 x13 x15 x20 x22^3 x9 -

x14 x15 x20 x22^3 x9 - 3 x11 x19 x20 x22^3 x9 -

x12 x19 x20 x22^3 x9 - 3 x13 x19 x20 x22^3 x9 -

2 x14 x19 x20 x22^3 x9 + x15 x19 x20 x22^3 x9 -

3 x11 x20^2 x22^3 x9 - x12 x20^2 x22^3 x9 - 3 x13 x20^2 x22^3 x9 -

2 x15 x20^2 x22^3 x9,

10 - 3 x12 x13 x14 x15 - 9 x12^2 x15^2 - 2 x12 x13 x15^2 +

3 x12 x14 x15^2 + 9 x13 x14 x15^2 - 5 x12 x13 x14 x19 +

4 x12^2 x15 x19 + 3 x12 x13 x15 x19 + 3 x12 x14 x15 x19 +

x13 x14 x15 x19 + 16 x11 x15^2 x19 + 9 x12 x15^2 x19 +

21 x13 x15^2 x19 + 8 x14 x15^2 x19 - 2 x12 x13 x14 x20 -

8 x12^2 x15 x20 + 2 x12 x13 x15 x20 + 2 x12 x14 x15 x20 +

14 x13 x14 x15 x20 + 2 x11 x15^2 x20 + 9 x12 x15^2 x20 +

8 x13 x15^2 x20 + 3 x14 x15^2 x20 + 3 x12^2 x19 x20 +

2 x12 x13 x19 x20 + 4 x10 x14 x19 x20 + 3 x12 x14 x19 x20 -

6 x13 x14 x19 x20 - 16 x10 x15 x19 x20 + 14 x11 x15 x19 x20 +

10 x12 x15 x19 x20 + 22 x13 x15 x19 x20 + 8 x14 x15 x19 x20 -

28 x15^2 x19 x20 - 6 x12^2 x20^2 + 2 x12 x13 x20^2 -

4 x10 x14 x20^2 + 7 x13 x14 x20^2 + 4 x10 x15 x20^2 +

16 x11 x15 x20^2 + 11 x12 x15 x20^2 + 15 x13 x15 x20^2 +

3 x14 x15 x20^2 - 16 x15^2 x20^2 + 12 x11 x19 x20^2 +

6 x12 x19 x20^2 + 13 x13 x19 x20^2 + 5 x14 x19 x20^2 -

13 x15 x19 x20^2 + 3 x12 x13 x14 x15^2 x19 x20^2 +

x12 x13 x14 x22 - 4 x12^2 x15 x22 - x12 x13 x15 x22 +

3 x12 x14 x15 x22 + x13 x14 x15 x22 - 8 x11 x15^2 x22 -

2 x12 x15^2 x22 - x13 x15^2 x22 - x14 x15^2 x22 -

3 x12^2 x19 x22 - 3 x12 x13 x19 x22 + 12 x10 x14 x19 x22 +

5 x12 x14 x19 x22 - 6 x13 x14 x19 x22 + 2 x11 x15 x19 x22 +

5 x12 x15 x19 x22 - x13 x15 x19 x22 + 3 x14 x15 x19 x22 -

14 x15^2 x19 x22 - 3 x12^2 x20 x22 - x12 x13 x20 x22 +

4 x10 x14 x20 x22 + 2 x12 x14 x20 x22 - 3 x13 x14 x20 x22 +

8 x10 x15 x20 x22 - 2 x11 x15 x20 x22 + 2 x12 x15 x20 x22 +

2 x13 x15 x20 x22 - 6 x14 x15 x20 x22 - 11 x15^2 x20 x22 +

12 x10 x19 x20 x22 + 16 x11 x19 x20 x22 + 4 x12 x19 x20 x22 +

x13 x19 x20 x22 + 10 x14 x19 x20 x22 - 12 x15 x19 x20 x22 +

3 x12 x13 x14 x15^2 x19 x20 x22 - 8 x11 x20^2 x22 -

8 x12 x20^2 x22 - 6 x13 x20^2 x22 + x14 x20^2 x22 -

7 x15 x20^2 x22 - 2 x12 x13 x14 x15^2 x20^2 x22 -

11 x19 x20^2 x22 + 3 x12 x13 x14 x15 x19 x20^2 x22 +

2 x12^2 x15^2 x19 x20^2 x22 - 3 x12 x14 x15^2 x19 x20^2 x22 -

3 x13 x14 x15^2 x19 x20^2 x22 - 3 x12^2 x22^2 - x12 x14 x22^2 -

x13 x14 x22^2 + 12 x10 x15 x22^2 - 2 x11 x15 x22^2 -

3 x12 x15 x22^2 - 5 x13 x15 x22^2 - x14 x15 x22^2 +

4 x15^2 x22^2 + 12 x10 x19 x22^2 + 8 x11 x19 x22^2 +

3 x12 x19 x22^2 - x13 x19 x22^2 + 6 x14 x19 x22^2 +

7 x15 x19 x22^2 - 3 x12 x13 x14 x15^2 x19 x22^2 +

12 x10 x20 x22^2 - 5 x12 x20 x22^2 - 8 x13 x20 x22^2 +

3 x14 x20 x22^2 + 4 x15 x20 x22^2 -

4 x12 x13 x14 x15^2 x20 x22^2 + 7 x12^2 x15^2 x19 x20 x22^2 +

6 x12 x13 x15^2 x19 x20 x22^2 - 3 x12 x14 x15^2 x19 x20 x22^2 -

6 x13 x14 x15^2 x19 x20 x22^2 + 2 x20^2 x22^2 -

x12 x13 x14 x15 x20^2 x22^2 + 2 x12 x13 x15^2 x20^2 x22^2 +

2 x12 x14 x15^2 x20^2 x22^2 - x13 x14 x15^2 x20^2 x22^2 -

3 x12 x13 x14 x19 x20^2 x22^2 + 4 x12^2 x15 x19 x20^2 x22^2 +

3 x12 x13 x15 x19 x20^2 x22^2 - 3 x12 x14 x15 x19 x20^2 x22^2 -

3 x13 x14 x15 x19 x20^2 x22^2 + 6 x11 x15^2 x19 x20^2 x22^2 +

2 x12 x15^2 x19 x20^2 x22^2 + 9 x13 x15^2 x19 x20^2 x22^2 +

3 x14 x15^2 x19 x20^2 x22^2 - 12 x10 x22^3 - 28 x11 x22^3 -

12 x12 x22^3 - 17 x13 x22^3 + x14 x22^3 - x15 x22^3 -

3 x12 x13 x14 x15^2 x22^3 - 14 x19 x22^3 -

3 x12 x13 x14 x15 x19 x22^3 + 3 x12^2 x15^2 x19 x22^3 +

3 x12 x13 x15^2 x19 x22^3 + 3 x12 x14 x15^2 x19 x22^3 -

13 x20 x22^3 - 2 x12 x13 x14 x15 x20 x22^3 -

3 x12^2 x15^2 x20 x22^3 + x12 x13 x15^2 x20 x22^3 +

4 x12 x14 x15^2 x20 x22^3 + x13 x14 x15^2 x20 x22^3 -

3 x12 x13 x14 x19 x20 x22^3 + 8 x12^2 x15 x19 x20 x22^3 +

6 x12 x13 x15 x19 x20 x22^3 + 18 x11 x15^2 x19 x20 x22^3 +

4 x12 x15^2 x19 x20 x22^3 + 15 x13 x15^2 x19 x20 x22^3 +

6 x14 x15^2 x19 x20 x22^3 + x12 x13 x15 x20^2 x22^3 +

x12 x14 x15 x20^2 x22^3 + x13 x14 x15 x20^2 x22^3 +

6 x11 x15^2 x20^2 x22^3 + 4 x12 x15^2 x20^2 x22^3 +

4 x13 x15^2 x20^2 x22^3 + x14 x15^2 x20^2 x22^3 +

3 x12 x14 x19 x20^2 x22^3 + 3 x13 x14 x19 x20^2 x22^3 +

12 x11 x15 x19 x20^2 x22^3 + x12 x15 x19 x20^2 x22^3 +

9 x13 x15 x19 x20^2 x22^3 + 3 x14 x15 x19 x20^2 x22^3 -

7 x15^2 x19 x20^2 x22^3 + 4 x12 x13 x14 x8 - 4 x14 x15^2 x8 -

4 x13 x14 x19 x8 + 4 x13 x15 x19 x8 + 4 x14 x15 x19 x8 -

4 x15^2 x19 x8 - 4 x12 x13 x20 x8 + 8 x13 x15 x20 x8 -

4 x15^2 x20 x8 + 4 x13 x20^2 x8 - 4 x15 x20^2 x8 -

4 x12 x14 x22 x8 + 4 x13 x15 x22 x8 + 4 x14 x15 x22 x8 -

4 x15^2 x22 x8 + 4 x12 x20 x22 x8 + 4 x13 x20 x22 x8 -

8 x15 x20 x22 x8 + 4 x13 x22^2 x8 - 4 x15 x22^2 x8 +

x12 x13 x14 x9 + 4 x12^2 x15 x9 + 2 x12 x13 x15 x9 -

2 x12 x14 x15 x9 - 4 x13 x14 x15 x9 + 2 x11 x15^2 x9 +

x12 x15^2 x9 + 3 x13 x15^2 x9 - x14 x15^2 x9 + 2 x12^2 x19 x9 +

x12 x13 x19 x9 - x12 x14 x19 x9 - 3 x13 x14 x19 x9 -

8 x11 x15 x19 x9 - 4 x12 x15 x19 x9 - 6 x13 x15 x19 x9 -

2 x14 x15 x19 x9 + 5 x15^2 x19 x9 + 3 x12^2 x20 x9 -

x12 x13 x20 x9 - 3 x13 x14 x20 x9 - 2 x11 x15 x20 x9 -

4 x12 x15 x20 x9 + 2 x13 x15 x20 x9 + 5 x15^2 x20 x9 -

4 x11 x19 x20 x9 - 2 x12 x19 x20 x9 - x13 x19 x20 x9 +

4 x15 x19 x20 x9 - 3 x12 x13 x14 x15^2 x19 x20 x9 +

3 x13 x20^2 x9 + 8 x15 x20^2 x9 - 3 x12 x13 x14 x15^2 x20^2 x9 +

x19 x20^2 x9 + 3 x12^2 x15^2 x19 x20^2 x9 +

3 x12 x13 x15^2 x19 x20^2 x9 - 3 x13 x14 x15^2 x19 x20^2 x9 -

x12 x14 x22 x9 - 2 x12 x15 x22 x9 + 4 x14 x15 x22 x9 -

x15^2 x22 x9 + 4 x11 x19 x22 x9 + x12 x19 x22 x9 +

4 x13 x19 x22 x9 + 3 x14 x19 x22 x9 + 6 x15 x19 x22 x9 +

4 x11 x20 x22 x9 + 3 x12 x20 x22 x9 + 4 x13 x20 x22 x9 +

3 x14 x20 x22 x9 + 4 x15 x20 x22 x9 + 4 x19 x20 x22 x9 -

3 x12^2 x15^2 x19 x20 x22 x9 + 3 x12 x14 x15^2 x19 x20 x22 x9 -

2 x20^2 x22 x9 + 2 x12 x13 x14 x15 x20^2 x22 x9 -

5 x12^2 x15^2 x20^2 x22 x9 - 3 x12 x13 x15^2 x20^2 x22 x9 +

3 x12 x14 x15^2 x20^2 x22 x9 + x13 x14 x15^2 x20^2 x22 x9 +

x12 x13 x14 x19 x20^2 x22 x9 + 2 x13 x14 x15 x19 x20^2 x22 x9 +

8 x11 x15^2 x19 x20^2 x22 x9 + 5 x12 x15^2 x19 x20^2 x22 x9 +

5 x13 x15^2 x19 x20^2 x22 x9 + 3 x14 x15^2 x19 x20^2 x22 x9 +

4 x11 x22^2 x9 + 2 x12 x22^2 x9 + 4 x13 x22^2 x9 + 8 x15 x22^2 x9 +

x20 x22^2 x9 + 2 x12 x13 x14 x15 x20 x22^2 x9 -

5 x12^2 x15^2 x20 x22^2 x9 - 3 x12 x13 x15^2 x20 x22^2 x9 +

x13 x14 x15^2 x20 x22^2 x9 + x12 x13 x14 x19 x20 x22^2 x9 +

2 x13 x14 x15 x19 x20 x22^2 x9 + 2 x11 x15^2 x19 x20 x22^2 x9 +

2 x12 x15^2 x19 x20 x22^2 x9 - x13 x15^2 x19 x20 x22^2 x9 -

2 x12 x14 x15 x20^2 x22^2 x9 + 3 x12 x15^2 x20^2 x22^2 x9 -

x14 x15^2 x20^2 x22^2 x9 + x12^2 x19 x20^2 x22^2 x9 -

x12 x14 x19 x20^2 x22^2 x9 - 2 x11 x15 x19 x20^2 x22^2 x9 -

2 x13 x15 x19 x20^2 x22^2 x9 - 2 x14 x15 x19 x20^2 x22^2 x9 -

2 x15^2 x19 x20^2 x22^2 x9 - 6 x22^3 x9 +

2 x12 x13 x14 x15 x22^3 x9 - 2 x12^2 x15^2 x22^3 x9 -

3 x12 x13 x15^2 x22^3 x9 + x13 x14 x15^2 x22^3 x9 +

x12 x13 x14 x19 x22^3 x9 + 2 x13 x14 x15 x19 x22^3 x9 +

2 x11 x15^2 x19 x22^3 x9 + 2 x12 x15^2 x19 x22^3 x9 -

x13 x15^2 x19 x22^3 x9 - 2 x12 x14 x15 x20 x22^3 x9 -

6 x11 x15^2 x20 x22^3 x9 - 3 x12 x15^2 x20 x22^3 x9 -

6 x13 x15^2 x20 x22^3 x9 - x14 x15^2 x20 x22^3 x9 +

x12^2 x19 x20 x22^3 x9 - x12 x14 x19 x20 x22^3 x9 -

2 x11 x15 x19 x20 x22^3 x9 - 2 x13 x15 x19 x20 x22^3 x9 -

2 x14 x15 x19 x20 x22^3 x9 - 2 x15^2 x19 x20 x22^3 x9 +

x12^2 x20^2 x22^3 x9 - 2 x11 x15 x20^2 x22^3 x9 -

2 x13 x15 x20^2 x22^3 x9 - 5 x15^2 x20^2 x22^3 x9,

x12 x13 x14 - 5 x12^2 x15 - x12 x13 x15 + x12 x14 x15 +

5 x13 x14 x15 - 7 x11 x15^2 + x14 x15^2 - 3 x13 x14 x19 -

12 x10 x15 x19 + 4 x11 x15 x19 + 5 x12 x15 x19 + 7 x13 x15 x19 +

x14 x15 x19 - 12 x15^2 x19 - 4 x12^2 x20 - x12 x13 x20 +

2 x13 x14 x20 - 4 x10 x15 x20 + 6 x12 x15 x20 + 3 x13 x15 x20 -

9 x15^2 x20 + 5 x11 x19 x20 + 4 x12 x19 x20 + 4 x13 x19 x20 -

11 x15 x19 x20 + x12 x13 x14 x15^2 x19 x20 + 4 x10 x20^2 +

10 x11 x20^2 + 4 x12 x20^2 + 4 x13 x20^2 - 6 x15 x20^2 +

2 x12 x13 x14 x15^2 x20^2 + 2 x19 x20^2 -

x12 x13 x14 x15 x19 x20^2 - x12^2 x15^2 x19 x20^2 -

x12 x13 x15^2 x19 x20^2 + 2 x13 x14 x15^2 x19 x20^2 - x12 x14 x22 +

x12 x15 x22 - 5 x14 x15 x22 + x15^2 x22 + 12 x10 x19 x22 +

15 x11 x19 x22 + 3 x13 x19 x22 + 3 x14 x19 x22 - 4 x15 x19 x22 +

12 x10 x20 x22 + 15 x11 x20 x22 + x12 x20 x22 + 3 x13 x20 x22 -

2 x14 x20 x22 + 7 x19 x20 x22 + x12^2 x15^2 x19 x20 x22 -

x12 x14 x15^2 x19 x20 x22 - 4 x20^2 x22 -

x12 x13 x14 x15 x20^2 x22 + 3 x12^2 x15^2 x20^2 x22 +

2 x12 x13 x15^2 x20^2 x22 - 2 x12 x14 x15^2 x20^2 x22 -

x13 x14 x15^2 x20^2 x22 - 2 x12^2 x15 x19 x20^2 x22 -

x12 x13 x15 x19 x20^2 x22 + x12 x14 x15 x19 x20^2 x22 -

x13 x14 x15 x19 x20^2 x22 - 6 x11 x15^2 x19 x20^2 x22 -

3 x12 x15^2 x19 x20^2 x22 - 4 x13 x15^2 x19 x20^2 x22 -

2 x14 x15^2 x19 x20^2 x22 + 12 x10 x22^2 + 15 x11 x22^2 +

3 x13 x22^2 - 5 x15 x22^2 - 6 x20 x22^2 -

x12 x13 x14 x15 x20 x22^2 + 3 x12^2 x15^2 x20 x22^2 +

2 x12 x13 x15^2 x20 x22^2 - x13 x14 x15^2 x20 x22^2 -

x12^2 x15 x19 x20 x22^2 - x12 x13 x15 x19 x20 x22^2 -

x13 x14 x15 x19 x20 x22^2 - 3 x11 x15^2 x19 x20 x22^2 -

2 x12 x15^2 x19 x20 x22^2 - x13 x15^2 x19 x20 x22^2 +

x12 x14 x15 x20^2 x22^2 - 2 x12 x15^2 x20^2 x22^2 +

x14 x15^2 x20^2 x22^2 - x12 x15 x19 x20^2 x22^2 +

x14 x15 x19 x20^2 x22^2 + 3 x15^2 x19 x20^2 x22^2 - 16 x22^3 -

x12 x13 x14 x15 x22^3 + 2 x12^2 x15^2 x22^3 +

2 x12 x13 x15^2 x22^3 - x13 x14 x15^2 x22^3 - x12^2 x15 x19 x22^3 -

x12 x13 x15 x19 x22^3 - x13 x14 x15 x19 x22^3 -

3 x11 x15^2 x19 x22^3 - 2 x12 x15^2 x19 x22^3 -

x13 x15^2 x19 x22^3 + x12^2 x15 x20 x22^3 +

x12 x14 x15 x20 x22^3 + 3 x11 x15^2 x20 x22^3 +

3 x13 x15^2 x20 x22^3 + x14 x15^2 x20 x22^3 -

x12 x15 x19 x20 x22^3 + x14 x15 x19 x20 x22^3 +

3 x15^2 x19 x20 x22^3 - 2 x12 x15 x20^2 x22^3 +

5 x15^2 x20^2 x22^3 + 4 x12^2 x8 + 4 x13 x15 x8 - 4 x15^2 x8 -

4 x12 x19 x8 - 4 x13 x19 x8 + 4 x15 x19 x8 - 4 x12 x20 x8 +

4 x19 x20 x8 + 4 x12^2 x9 + x12 x13 x9 - x12 x14 x9 -

2 x13 x14 x9 - x12 x15 x9 + x13 x15 x9 - x14 x15 x9 + 2 x15^2 x9 -

6 x11 x19 x9 - 4 x12 x19 x9 - 5 x13 x19 x9 - x14 x19 x9 -

x15 x19 x9 - x12 x13 x14 x15^2 x19 x9 - 3 x11 x20 x9 -

4 x12 x20 x9 - x13 x20 x9 + x15 x20 x9 -

2 x12 x13 x14 x15^2 x20 x9 + 2 x19 x20 x9 +

x12 x13 x14 x15 x19 x20 x9 + x12^2 x15^2 x19 x20 x9 +

x12 x13 x15^2 x19 x20 x9 - 2 x13 x14 x15^2 x19 x20 x9 +

4 x20^2 x9 - x12 x13 x14 x15 x20^2 x9 + 2 x12^2 x15^2 x20^2 x9 +

2 x12 x13 x15^2 x20^2 x9 - x13 x14 x15^2 x20^2 x9 -

x12^2 x15 x19 x20^2 x9 - x12 x13 x15 x19 x20^2 x9 -

x13 x14 x15 x19 x20^2 x9 - 3 x11 x15^2 x19 x20^2 x9 -

2 x12 x15^2 x19 x20^2 x9 - x13 x15^2 x19 x20^2 x9 - x12 x22 x9 +

2 x14 x22 x9 - x15 x22 x9 + 5 x19 x22 x9 - x12^2 x15^2 x19 x22 x9 +

x12 x14 x15^2 x19 x22 x9 + 4 x20 x22 x9 -

x12^2 x15^2 x20 x22 x9 + 2 x12 x14 x15^2 x20 x22 x9 +

x12^2 x15 x19 x20 x22 x9 - x12 x14 x15 x19 x20 x22 x9 +

3 x11 x15^2 x19 x20 x22 x9 + x12 x15^2 x19 x20 x22 x9 +

3 x13 x15^2 x19 x20 x22 x9 + 2 x14 x15^2 x19 x20 x22 x9 +

x12 x13 x14 x20^2 x22 x9 - x12^2 x15 x20^2 x22 x9 -

x12 x13 x15 x20^2 x22 x9 + x12 x14 x15 x20^2 x22 x9 +

x13 x14 x15 x20^2 x22 x9 + x11 x15^2 x20^2 x22 x9 +

x14 x15^2 x20^2 x22 x9 + x13 x14 x19 x20^2 x22 x9 +

4 x11 x15 x19 x20^2 x22 x9 + x12 x15 x19 x20^2 x22 x9 +

3 x13 x15 x19 x20^2 x22 x9 + x14 x15 x19 x20^2 x22 x9 +

6 x22^2 x9 - x12^2 x15^2 x22^2 x9 + x12 x13 x14 x20 x22^2 x9 -

x12^2 x15 x20 x22^2 x9 - x12 x13 x15 x20 x22^2 x9 +

x13 x14 x15 x20 x22^2 x9 + x11 x15^2 x20 x22^2 x9 +

2 x12 x15^2 x20 x22^2 x9 + x13 x14 x19 x20 x22^2 x9 +

4 x11 x15 x19 x20 x22^2 x9 + 2 x12 x15 x19 x20 x22^2 x9 +

3 x13 x15 x19 x20 x22^2 x9 - 3 x15^2 x19 x20 x22^2 x9 -

x12 x14 x20^2 x22^2 x9 + x12 x15 x20^2 x22^2 x9 -

x14 x15 x20^2 x22^2 x9 + x15^2 x20^2 x22^2 x9 -

x11 x19 x20^2 x22^2 x9 - x13 x19 x20^2 x22^2 x9 -

x14 x19 x20^2 x22^2 x9 - 4 x15 x19 x20^2 x22^2 x9 +

x12 x13 x14 x22^3 x9 - 2 x12^2 x15 x22^3 x9 -

x12 x13 x15 x22^3 x9 + x13 x14 x15 x22^3 x9 -

2 x11 x15^2 x22^3 x9 - 3 x13 x15^2 x22^3 x9 +

x13 x14 x19 x22^3 x9 + 4 x11 x15 x19 x22^3 x9 +

2 x12 x15 x19 x22^3 x9 + 3 x13 x15 x19 x22^3 x9 -

3 x15^2 x19 x22^3 x9 - x12 x14 x20 x22^3 x9 +

3 x12 x15 x20 x22^3 x9 - x14 x15 x20 x22^3 x9 -

4 x15^2 x20 x22^3 x9 - x11 x19 x20 x22^3 x9 -

x13 x19 x20 x22^3 x9 - x14 x19 x20 x22^3 x9 -

4 x15 x19 x20 x22^3 x9 - x11 x20^2 x22^3 x9 - x13 x20^2 x22^3 x9 -

5 x15 x20^2 x22^3 x9,

2 x11 x15^2 + 3 x10 x15 x19 + x11 x15 x19 + 3 x15^2 x19 +

x10 x15 x20 + 2 x11 x15 x20 + 2 x15^2 x20 - x11 x19 x20 +

3 x15 x19 x20 - x10 x20^2 - x11 x20^2 + x15 x20^2 -

3 x10 x19 x22 - 3 x11 x19 x22 - x15 x19 x22 - 3 x10 x20 x22 -

3 x11 x20 x22 - x15 x20 x22 - 2 x19 x20 x22 - 3 x10 x22^2 -

3 x11 x22^2 - x15 x22^2 + 2 x22^3 + x11 x15 x8 + x15^2 x8 -

x11 x19 x8 + x15 x20 x8 + x20^2 x8 + x19 x22 x8 + x20 x22 x8 +

x22^2 x8, -x10 x15 - x11 x19 + x20^2 + x19 x22 + x20 x22 + x22^2 +

x10 x8 + x11 x8 + x15 x8 + x20 x8,

x12 x13 - x11 x19 - x13 x19 + x10 x20 + x11 x20 + x19 x20 +

2 x20^2 + x19 x22 + x20 x22 + x22^2 - x12 x8 - x10 x9 +

x8 x9, -x12 x13 + x13 x19 - x11 x20 - x19 x20 - x20^2 + x11 x8 +

x12 x8 + x8^2, -5 x12 x13 x14 x15 + x12 x13 x15^2 +

4 x13 x14 x15^2 - 2 x12 x13 x14 x19 + 4 x12^2 x15 x19 +

3 x12 x13 x15 x19 + 3 x12 x14 x15 x19 - x13 x14 x15 x19 +

4 x11 x15^2 x19 + 8 x13 x15^2 x19 + x14 x15^2 x19 -

x12 x13 x14 x20 + 4 x12^2 x15 x20 + 4 x12 x13 x15 x20 +

2 x12 x14 x15 x20 + 2 x13 x14 x15 x20 + 8 x11 x15^2 x20 +

3 x12 x15^2 x20 + 3 x13 x15^2 x20 - x14 x15^2 x20 -

x12 x13 x19 x20 + 4 x10 x14 x19 x20 + 3 x12 x14 x19 x20 -

x13 x14 x19 x20 - 4 x10 x15 x19 x20 + 4 x11 x15 x19 x20 -

2 x12 x15 x19 x20 + 10 x13 x15 x19 x20 + 8 x14 x15 x19 x20 -

9 x15^2 x19 x20 + x12 x13 x20^2 - 4 x10 x14 x20^2 +

4 x13 x14 x20^2 + 4 x10 x15 x20^2 + 8 x11 x15 x20^2 -

x12 x15 x20^2 + 7 x13 x15 x20^2 - x14 x15 x20^2 + 2 x15^2 x20^2 -

4 x10 x19 x20^2 + 4 x13 x19 x20^2 + 5 x14 x19 x20^2 -

9 x15 x19 x20^2 + x12 x13 x14 x22 - 4 x12^2 x15 x22 -

x12 x13 x15 x22 + 5 x12 x14 x15 x22 + x13 x14 x15 x22 -

8 x11 x15^2 x22 - 5 x12 x15^2 x22 - 5 x13 x15^2 x22 -

3 x12 x13 x19 x22 + 12 x10 x14 x19 x22 + 2 x12 x14 x19 x22 -

6 x13 x14 x19 x22 - 12 x10 x15 x19 x22 + 5 x12 x15 x19 x22 +

5 x13 x15 x19 x22 + 9 x14 x15 x19 x22 - 16 x15^2 x19 x22 -

x12 x13 x20 x22 + 4 x10 x14 x20 x22 + x12 x14 x20 x22 -

3 x13 x14 x20 x22 - 4 x10 x15 x20 x22 - 4 x11 x15 x20 x22 +

4 x13 x15 x20 x22 + 6 x14 x15 x20 x22 - 11 x15^2 x20 x22 -

8 x10 x19 x20 x22 - 8 x11 x19 x20 x22 + x12 x19 x20 x22 -

7 x13 x19 x20 x22 + 5 x14 x19 x20 x22 - 14 x15 x19 x20 x22 +

3 x12 x13 x14 x15^2 x19 x20 x22 - 12 x10 x20^2 x22 -

4 x11 x20^2 x22 - x12 x20^2 x22 + 3 x13 x20^2 x22 +

8 x14 x20^2 x22 - 23 x15 x20^2 x22 + x12 x13 x14 x15^2 x20^2 x22 +

3 x12 x13 x14 x15 x19 x20^2 x22 - 4 x12^2 x15^2 x19 x20^2 x22 -

3 x12 x13 x15^2 x19 x20^2 x22 - x12 x14 x22^2 - x13 x14 x22^2 -

4 x11 x15 x22^2 - 3 x12 x15 x22^2 - 3 x13 x15 x22^2 -

x14 x15 x22^2 + 9 x15^2 x22^2 + 12 x10 x19 x22^2 +

8 x11 x19 x22^2 + 3 x12 x19 x22^2 - x13 x19 x22^2 +

6 x14 x19 x22^2 + 7 x15 x19 x22^2 -

3 x12 x13 x14 x15^2 x19 x22^2 + 4 x11 x20 x22^2 + x12 x20 x22^2 +

x13 x20 x22^2 + 7 x14 x20 x22^2 + 4 x15 x20 x22^2 -

x12 x13 x14 x15^2 x20 x22^2 + 19 x19 x20 x22^2 +

4 x12^2 x15^2 x19 x20 x22^2 + 3 x12 x13 x15^2 x19 x20 x22^2 -

3 x12 x14 x15^2 x19 x20 x22^2 - 3 x13 x14 x15^2 x19 x20 x22^2 +

9 x20^2 x22^2 - x12 x13 x14 x15 x20^2 x22^2 +

2 x12 x13 x15^2 x20^2 x22^2 - x12 x14 x15^2 x20^2 x22^2 -

x13 x14 x15^2 x20^2 x22^2 - 3 x12 x13 x14 x19 x20^2 x22^2 +

4 x12^2 x15 x19 x20^2 x22^2 + 3 x12 x13 x15 x19 x20^2 x22^2 -

3 x12 x14 x15 x19 x20^2 x22^2 - 3 x13 x14 x15 x19 x20^2 x22^2 -

x12 x15^2 x19 x20^2 x22^2 + 3 x13 x15^2 x19 x20^2 x22^2 -

4 x10 x22^3 + 5 x14 x22^3 - 5 x15 x22^3 + 5 x19 x22^3 -

3 x12 x13 x14 x15 x19 x22^3 + 3 x12 x14 x15^2 x19 x22^3 +

3 x13 x14 x15^2 x19 x22^3 + 7 x20 x22^3 -

2 x12 x13 x14 x15 x20 x22^3 + x12 x13 x15^2 x20 x22^3 +

x12 x14 x15^2 x20 x22^3 + x13 x14 x15^2 x20 x22^3 -

3 x12 x13 x14 x19 x20 x22^3 + 8 x12^2 x15 x19 x20 x22^3 +

6 x12 x13 x15 x19 x20 x22^3 + 12 x11 x15^2 x19 x20 x22^3 +

x12 x15^2 x19 x20 x22^3 + 9 x13 x15^2 x19 x20 x22^3 +

3 x14 x15^2 x19 x20 x22^3 + x12 x13 x15 x20^2 x22^3 +

x12 x14 x15 x20^2 x22^3 + x13 x14 x15 x20^2 x22^3 -

2 x12 x15^2 x20^2 x22^3 - 2 x13 x15^2 x20^2 x22^3 +

x14 x15^2 x20^2 x22^3 + 3 x12 x14 x19 x20^2 x22^3 +

3 x13 x14 x19 x20^2 x22^3 + 12 x11 x15 x19 x20^2 x22^3 +

x12 x15 x19 x20^2 x22^3 + 9 x13 x15 x19 x20^2 x22^3 +

3 x14 x15 x19 x20^2 x22^3 - 7 x15^2 x19 x20^2 x22^3 +

4 x13 x15^2 x7 + 4 x14 x15^2 x7 - 4 x13 x15 x19 x7 -

4 x14 x15 x19 x7 + 4 x15^2 x19 x7 + 4 x15 x19 x20 x7 +

4 x15 x20^2 x7 - 4 x13 x15 x22 x7 - 4 x14 x15 x22 x7 +

4 x15^2 x22 x7 + 4 x13 x19 x22 x7 + 4 x14 x19 x22 x7 -

4 x15 x19 x22 x7 + 4 x15 x20 x22 x7 - 4 x19 x20 x22 x7 -

4 x20^2 x22 x7 - 4 x20 x22^2 x7 - 4 x22^3 x7 + 4 x13 x15^2 x9 +

4 x14 x15^2 x9 - 4 x13 x15 x19 x9 - 4 x14 x15 x19 x9 +

4 x15^2 x19 x9 + 4 x15 x19 x20 x9 + 4 x15 x20^2 x9 -

4 x13 x15 x22 x9 - 4 x14 x15 x22 x9 + 4 x15^2 x22 x9 +

4 x13 x19 x22 x9 + 4 x14 x19 x22 x9 - 4 x15 x19 x22 x9 +

4 x15 x20 x22 x9 - 4 x19 x20 x22 x9 - 4 x20^2 x22 x9 -

4 x20 x22^2 x9 - 4 x22^3 x9, -4 + x12 x13 x14 x15 + 4 x12^2 x15^2 -

x12 x13 x15^2 - 4 x13 x14 x15^2 + 6 x12 x13 x14 x19 -

4 x12^2 x15 x19 - 3 x12 x13 x15 x19 - 3 x12 x14 x15 x19 +

x13 x14 x15 x19 - 8 x11 x15^2 x19 - 4 x12 x15^2 x19 -

12 x13 x15^2 x19 - x14 x15^2 x19 + x12 x13 x14 x20 +

4 x12^2 x15 x20 - 2 x12 x14 x15 x20 - 6 x13 x14 x15 x20 -

4 x11 x15^2 x20 - 7 x12 x15^2 x20 - 7 x13 x15^2 x20 +

x14 x15^2 x20 - 4 x12^2 x19 x20 - 3 x12 x13 x19 x20 -

4 x10 x14 x19 x20 - 3 x12 x14 x19 x20 + 5 x13 x14 x19 x20 +

16 x10 x15 x19 x20 - 4 x11 x15 x19 x20 - 6 x12 x15 x19 x20 -

18 x13 x15 x19 x20 - 8 x14 x15 x19 x20 + 25 x15^2 x19 x20 +

4 x12^2 x20^2 - x12 x13 x20^2 + 4 x10 x14 x20^2 -

4 x13 x14 x20^2 - 4 x10 x15 x20^2 - 8 x11 x15 x20^2 -

7 x12 x15 x20^2 - 11 x13 x15 x20^2 + x14 x15 x20^2 +

6 x15^2 x20^2 - 12 x11 x19 x20^2 - 4 x12 x19 x20^2 -

12 x13 x19 x20^2 - 5 x14 x19 x20^2 + 21 x15 x19 x20^2 -

x12 x13 x14 x22 + 4 x12^2 x15 x22 + x12 x13 x15 x22 -

x12 x14 x15 x22 - x13 x14 x15 x22 + 8 x11 x15^2 x22 +

5 x12 x15^2 x22 + 5 x13 x15^2 x22 + 4 x12^2 x19 x22 +

3 x12 x13 x19 x22 - 12 x10 x14 x19 x22 - 6 x12 x14 x19 x22 +

6 x13 x14 x19 x22 - 8 x11 x15 x19 x22 - 5 x12 x15 x19 x22 -

5 x13 x15 x19 x22 - 9 x14 x15 x19 x22 + 12 x15^2 x19 x22 +

4 x12^2 x20 x22 + x12 x13 x20 x22 - 4 x10 x14 x20 x22 -

x12 x14 x20 x22 + 3 x13 x14 x20 x22 - 8 x10 x15 x20 x22 -

4 x11 x15 x20 x22 - 4 x12 x15 x20 x22 - 4 x13 x15 x20 x22 -

2 x14 x15 x20 x22 + 7 x15^2 x20 x22 - 12 x10 x19 x20 x22 -

16 x11 x19 x20 x22 - 5 x12 x19 x20 x22 - x13 x19 x20 x22 -

9 x14 x19 x20 x22 + 2 x15 x19 x20 x22 -

3 x12 x13 x14 x15^2 x19 x20 x22 + 5 x12 x20^2 x22 +

x13 x20^2 x22 - 8 x14 x20^2 x22 + 7 x15 x20^2 x22 -

x12 x13 x14 x15^2 x20^2 x22 - 3 x12 x13 x14 x15 x19 x20^2 x22 +

4 x12^2 x15^2 x19 x20^2 x22 + 3 x12 x13 x15^2 x19 x20^2 x22 +

4 x12^2 x22^2 + x12 x14 x22^2 + x13 x14 x22^2 - 12 x10 x15 x22^2 -

4 x11 x15 x22^2 + 3 x12 x15 x22^2 + 3 x13 x15 x22^2 +

x14 x15 x22^2 - 13 x15^2 x22^2 - 12 x10 x19 x22^2 -

8 x11 x19 x22^2 - 3 x12 x19 x22^2 + x13 x19 x22^2 -

6 x14 x19 x22^2 - 7 x15 x19 x22^2 +

3 x12 x13 x14 x15^2 x19 x22^2 - 12 x10 x20 x22^2 -

8 x11 x20 x22^2 + 3 x12 x20 x22^2 + 3 x13 x20 x22^2 -

7 x14 x20 x22^2 - 16 x15 x20 x22^2 + x12 x13 x14 x15^2 x20 x22^2 -

11 x19 x20 x22^2 - 4 x12^2 x15^2 x19 x20 x22^2 -

3 x12 x13 x15^2 x19 x20 x22^2 + 3 x12 x14 x15^2 x19 x20 x22^2 +

3 x13 x14 x15^2 x19 x20 x22^2 - 9 x20^2 x22^2 +

x12 x13 x14 x15 x20^2 x22^2 - 2 x12 x13 x15^2 x20^2 x22^2 +

x12 x14 x15^2 x20^2 x22^2 + x13 x14 x15^2 x20^2 x22^2 +

3 x12 x13 x14 x19 x20^2 x22^2 - 4 x12^2 x15 x19 x20^2 x22^2 -

3 x12 x13 x15 x19 x20^2 x22^2 + 3 x12 x14 x15 x19 x20^2 x22^2 +

3 x13 x14 x15 x19 x20^2 x22^2 + x12 x15^2 x19 x20^2 x22^2 -

3 x13 x15^2 x19 x20^2 x22^2 + 12 x10 x22^3 + 20 x11 x22^3 +

12 x12 x22^3 + 12 x13 x22^3 - 5 x14 x22^3 + 5 x15 x22^3 +

3 x19 x22^3 + 3 x12 x13 x14 x15 x19 x22^3 -

3 x12 x14 x15^2 x19 x22^3 - 3 x13 x14 x15^2 x19 x22^3 +

5 x20 x22^3 + 2 x12 x13 x14 x15 x20 x22^3 -

x12 x13 x15^2 x20 x22^3 - x12 x14 x15^2 x20 x22^3 -

x13 x14 x15^2 x20 x22^3 + 3 x12 x13 x14 x19 x20 x22^3 -

8 x12^2 x15 x19 x20 x22^3 - 6 x12 x13 x15 x19 x20 x22^3 -

12 x11 x15^2 x19 x20 x22^3 - x12 x15^2 x19 x20 x22^3 -

9 x13 x15^2 x19 x20 x22^3 - 3 x14 x15^2 x19 x20 x22^3 -

x12 x13 x15 x20^2 x22^3 - x12 x14 x15 x20^2 x22^3 -

x13 x14 x15 x20^2 x22^3 + 2 x12 x15^2 x20^2 x22^3 +

2 x13 x15^2 x20^2 x22^3 - x14 x15^2 x20^2 x22^3 -

3 x12 x14 x19 x20^2 x22^3 - 3 x13 x14 x19 x20^2 x22^3 -

12 x11 x15 x19 x20^2 x22^3 - x12 x15 x19 x20^2 x22^3 -

9 x13 x15 x19 x20^2 x22^3 - 3 x14 x15 x19 x20^2 x22^3 +

7 x15^2 x19 x20^2 x22^3 + 4 x13 x14 x15 x7 - 4 x14 x15^2 x7 -

4 x13 x14 x19 x7 + 4 x13 x15 x19 x7 + 4 x14 x15 x19 x7 -

4 x15^2 x19 x7 + 4 x13 x15 x20 x7 - 4 x15^2 x20 x7 +

4 x13 x20^2 x7 - 4 x15 x20^2 x7 + 4 x13 x15 x22 x7 -

4 x15^2 x22 x7 + 4 x13 x20 x22 x7 - 4 x15 x20 x22 x7 +

4 x13 x22^2 x7 - 4 x15 x22^2 x7 + 4 x13 x14 x15 x9 -

4 x14 x15^2 x9 - 4 x13 x14 x19 x9 + 4 x13 x15 x19 x9 +

4 x14 x15 x19 x9 - 4 x15^2 x19 x9 + 4 x13 x15 x20 x9 -

4 x15^2 x20 x9 + 4 x13 x20^2 x9 - 4 x15 x20^2 x9 +

4 x13 x15 x22 x9 - 4 x15^2 x22 x9 + 4 x13 x20 x22 x9 -

4 x15 x20 x22 x9 + 4 x13 x22^2 x9 - 4 x15 x22^2 x9,

5 x12^2 x15 + 5 x12 x13 x15 - 5 x13 x14 x15 + 15 x11 x15^2 +

5 x12 x15^2 + 11 x13 x15^2 + 6 x14 x15^2 + 4 x12^2 x19 +

4 x12 x13 x19 - 4 x13 x14 x19 + 12 x10 x15 x19 - 6 x12 x15 x19 -

8 x13 x15 x19 - 3 x14 x15 x19 + 26 x15^2 x19 + 3 x12^2 x20 +

3 x12 x13 x20 - 3 x13 x14 x20 + 4 x10 x15 x20 + 10 x11 x15 x20 -

x12 x15 x20 + 2 x13 x15 x20 + 3 x14 x15 x20 + 11 x15^2 x20 -

3 x11 x19 x20 + x13 x19 x20 + 3 x14 x19 x20 + 17 x15 x19 x20 -

4 x10 x20^2 + 2 x11 x20^2 + 2 x12 x20^2 + 6 x13 x20^2 +

3 x14 x20^2 + 13 x15 x20^2 + 5 x19 x20^2 + 5 x14 x15 x22 -

12 x10 x19 x22 - 9 x11 x19 x22 + 2 x12 x19 x22 + 3 x13 x19 x22 +

4 x14 x19 x22 - 6 x15 x19 x22 - 12 x10 x20 x22 - 9 x11 x20 x22 +

2 x12 x20 x22 + 3 x13 x20 x22 + 3 x14 x20 x22 - 5 x15 x20 x22 -

6 x19 x20 x22 - 6 x12^2 x15^2 x19 x20 x22 -

6 x12 x13 x15^2 x19 x20 x22 + 6 x13 x14 x15^2 x19 x20 x22 -

7 x20^2 x22 - 6 x12^2 x15 x19 x20^2 x22 -

6 x12 x13 x15 x19 x20^2 x22 + 6 x13 x14 x15 x19 x20^2 x22 -

6 x11 x15^2 x19 x20^2 x22 - 6 x13 x15^2 x19 x20^2 x22 -

12 x10 x22^2 - 9 x11 x22^2 + 2 x12 x22^2 + 3 x13 x22^2 +

3 x19 x22^2 - 4 x20 x22^2 - 3 x12^2 x15 x19 x20 x22^2 -

3 x12 x13 x15 x19 x20 x22^2 + 3 x13 x14 x15 x19 x20 x22^2 -

9 x11 x15^2 x19 x20 x22^2 - 3 x12 x15^2 x19 x20 x22^2 -

9 x13 x15^2 x19 x20 x22^2 - 6 x14 x15^2 x19 x20 x22^2 +

3 x12^2 x19 x20^2 x22^2 + 3 x12 x13 x19 x20^2 x22^2 -

3 x13 x14 x19 x20^2 x22^2 - 6 x11 x15 x19 x20^2 x22^2 -

3 x12 x15 x19 x20^2 x22^2 - 6 x13 x15 x19 x20^2 x22^2 -

6 x14 x15 x19 x20^2 x22^2 + 9 x15^2 x19 x20^2 x22^2 + x22^3 +

6 x12^2 x15^2 x22^3 + 6 x12 x13 x15^2 x22^3 -

6 x13 x14 x15^2 x22^3 - 3 x12^2 x15 x19 x22^3 -

3 x12 x13 x15 x19 x22^3 + 3 x13 x14 x15 x19 x22^3 -

9 x11 x15^2 x19 x22^3 - 3 x12 x15^2 x19 x22^3 -

9 x13 x15^2 x19 x22^3 + 3 x12^2 x15 x20 x22^3 +

3 x12 x13 x15 x20 x22^3 - 3 x13 x14 x15 x20 x22^3 -

3 x11 x15^2 x20 x22^3 - 3 x12 x15^2 x20 x22^3 -

3 x13 x15^2 x20 x22^3 + 3 x12^2 x19 x20 x22^3 +

3 x12 x13 x19 x20 x22^3 - 3 x13 x14 x19 x20 x22^3 -

6 x11 x15 x19 x20 x22^3 - 3 x12 x15 x19 x20 x22^3 -

6 x13 x15 x19 x20 x22^3 - 3 x14 x15 x19 x20 x22^3 +

3 x15^2 x19 x20 x22^3 + 3 x12^2 x20^2 x22^3 +

3 x12 x13 x20^2 x22^3 - 3 x13 x14 x20^2 x22^3 -

6 x11 x15 x20^2 x22^3 - 3 x12 x15 x20^2 x22^3 -

6 x13 x15 x20^2 x22^3 + 3 x15^2 x20^2 x22^3 +

3 x14 x19 x20^2 x22^3 - 3 x15 x19 x20^2 x22^3 + 4 x12 x15 x7 +

4 x13 x15 x7 - 4 x15^2 x7 - 4 x12 x19 x7 - 4 x13 x19 x7 +

4 x15 x19 x7 - 4 x15 x20 x7 + 4 x19 x20 x7 - 2 x12^2 x9 -

2 x12 x13 x9 + 2 x13 x14 x9 + 3 x12 x15 x9 + 4 x13 x15 x9 +

2 x14 x15 x9 - 9 x15^2 x9 + 6 x11 x19 x9 + 2 x13 x19 x9 +

2 x14 x19 x9 + x15 x19 x9 + x11 x20 x9 + x12 x20 x9 + x13 x20 x9 -

7 x15 x20 x9 + x19 x20 x9 - 3 x12^2 x15^2 x19 x20 x9 -

3 x12 x13 x15^2 x19 x20 x9 + 3 x13 x14 x15^2 x19 x20 x9 -

6 x20^2 x9 - 3 x12^2 x15 x19 x20^2 x9 -

3 x12 x13 x15 x19 x20^2 x9 + 3 x13 x14 x15 x19 x20^2 x9 -

3 x11 x15^2 x19 x20^2 x9 - 3 x13 x15^2 x19 x20^2 x9 -

2 x14 x22 x9 + x15 x22 x9 - 3 x19 x22 x9 + x12^2 x15^2 x19 x22 x9 +

x12 x13 x15^2 x19 x22 x9 - x13 x14 x15^2 x19 x22 x9 -

3 x20 x22 x9 + x12^2 x15^2 x20 x22 x9 + x12 x13 x15^2 x20 x22 x9 -

x13 x14 x15^2 x20 x22 x9 - x12^2 x15 x19 x20 x22 x9 -

x12 x13 x15 x19 x20 x22 x9 + x13 x14 x15 x19 x20 x22 x9 -

5 x11 x15^2 x19 x20 x22 x9 - 2 x12 x15^2 x19 x20 x22 x9 -

5 x13 x15^2 x19 x20 x22 x9 - 3 x14 x15^2 x19 x20 x22 x9 +

x12^2 x15 x20^2 x22 x9 + x12 x13 x15 x20^2 x22 x9 -

x13 x14 x15 x20^2 x22 x9 + x11 x15^2 x20^2 x22 x9 +

x13 x15^2 x20^2 x22 x9 + 2 x12^2 x19 x20^2 x22 x9 +

2 x12 x13 x19 x20^2 x22 x9 - 2 x13 x14 x19 x20^2 x22 x9 -

4 x11 x15 x19 x20^2 x22 x9 - 2 x12 x15 x19 x20^2 x22 x9 -

4 x13 x15 x19 x20^2 x22 x9 - 3 x14 x15 x19 x20^2 x22 x9 +

5 x15^2 x19 x20^2 x22 x9 - 5 x22^2 x9 + x12^2 x15^2 x22^2 x9 +

x12 x13 x15^2 x22^2 x9 - x13 x14 x15^2 x22^2 x9 +

x14 x15^2 x19 x22^2 x9 + x12^2 x15 x20 x22^2 x9 +

x12 x13 x15 x20 x22^2 x9 - x13 x14 x15 x20 x22^2 x9 +

x11 x15^2 x20 x22^2 x9 + x13 x15^2 x20 x22^2 x9 +

x14 x15^2 x20 x22^2 x9 + 2 x12^2 x19 x20 x22^2 x9 +

2 x12 x13 x19 x20 x22^2 x9 - 2 x13 x14 x19 x20 x22^2 x9 -

x12 x15 x19 x20 x22^2 x9 - x14 x15 x19 x20 x22^2 x9 +

2 x15^2 x19 x20 x22^2 x9 + x14 x15 x20^2 x22^2 x9 -

x15^2 x20^2 x22^2 x9 + 3 x11 x19 x20^2 x22^2 x9 +

x12 x19 x20^2 x22^2 x9 + 3 x13 x19 x20^2 x22^2 x9 +

2 x14 x19 x20^2 x22^2 x9 + 2 x12^2 x15 x22^3 x9 +

2 x12 x13 x15 x22^3 x9 - 2 x13 x14 x15 x22^3 x9 +

6 x11 x15^2 x22^3 x9 + 2 x12 x15^2 x22^3 x9 +

6 x13 x15^2 x22^3 x9 + x14 x15^2 x22^3 x9 + 2 x12^2 x19 x22^3 x9 +

2 x12 x13 x19 x22^3 x9 - 2 x13 x14 x19 x22^3 x9 -

x12 x15 x19 x22^3 x9 + 3 x15^2 x19 x22^3 x9 +

4 x11 x15 x20 x22^3 x9 + x12 x15 x20 x22^3 x9 +

4 x13 x15 x20 x22^3 x9 + x14 x15 x20 x22^3 x9 +

3 x11 x19 x20 x22^3 x9 + x12 x19 x20 x22^3 x9 +

3 x13 x19 x20 x22^3 x9 + 2 x14 x19 x20 x22^3 x9 -

x15 x19 x20 x22^3 x9 + 3 x11 x20^2 x22^3 x9 + x12 x20^2 x22^3 x9 +

3 x13 x20^2 x22^3 x9 + 2 x15 x20^2 x22^3 x9,

2 + x12 x13 x14 x15 + 7 x12^2 x15^2 + 2 x12 x13 x15^2 -

3 x12 x14 x15^2 - 3 x13 x14 x15^2 + x12 x13 x14 x19 +

8 x12^2 x15 x19 + 3 x12 x13 x15 x19 - 9 x12 x14 x15 x19 -

7 x13 x14 x15 x19 - 8 x11 x15^2 x19 - 7 x12 x15^2 x19 -

9 x13 x15^2 x19 - 4 x14 x15^2 x19 + 10 x12^2 x15 x20 -

2 x12 x14 x15 x20 - 12 x13 x14 x15 x20 + 8 x11 x15^2 x20 -

x12 x15^2 x20 + 4 x13 x15^2 x20 + x14 x15^2 x20 + x12^2 x19 x20 +

2 x12 x13 x19 x20 - 4 x10 x14 x19 x20 - 3 x12 x14 x19 x20 +

16 x10 x15 x19 x20 - 6 x11 x15 x19 x20 - 6 x12 x15 x19 x20 -

12 x13 x15 x19 x20 - 8 x14 x15 x19 x20 + 34 x15^2 x19 x20 +

2 x12^2 x20^2 + 4 x10 x14 x20^2 - 7 x13 x14 x20^2 -

4 x10 x15 x20^2 + 5 x12 x15 x20^2 + 3 x13 x15 x20^2 +

x14 x15 x20^2 + 12 x15^2 x20^2 - 10 x11 x19 x20^2 -

2 x12 x19 x20^2 - 5 x13 x19 x20^2 - 5 x14 x19 x20^2 +

23 x15 x19 x20^2 - 9 x12 x13 x14 x15^2 x19 x20^2 -

x12 x13 x14 x22 + 4 x12^2 x15 x22 + x12 x13 x15 x22 -

x12 x14 x15 x22 - x13 x14 x15 x22 + 8 x11 x15^2 x22 +

2 x12 x15^2 x22 + 5 x13 x15^2 x22 - x14 x15^2 x22 -

x12^2 x19 x22 + 3 x12 x13 x19 x22 - 12 x10 x14 x19 x22 -

x12 x14 x19 x22 + 6 x13 x14 x19 x22 + 6 x11 x15 x19 x22 +

x12 x15 x19 x22 + 9 x13 x15 x19 x22 - x14 x15 x19 x22 -

x12^2 x20 x22 + x12 x13 x20 x22 - 4 x10 x14 x20 x22 +

3 x13 x14 x20 x22 - 8 x10 x15 x20 x22 + 10 x11 x15 x20 x22 +

8 x12 x15 x20 x22 + 10 x13 x15 x20 x22 + 4 x14 x15 x20 x22 -

x15^2 x20 x22 - 12 x10 x19 x20 x22 - 6 x11 x19 x20 x22 +

9 x13 x19 x20 x22 - 4 x14 x19 x20 x22 + 4 x15 x19 x20 x22 -

3 x12 x13 x14 x15^2 x19 x20 x22 + 2 x11 x20^2 x22 +

2 x12 x20^2 x22 - 5 x14 x20^2 x22 - x15 x20^2 x22 +

2 x12 x13 x14 x15^2 x20^2 x22 - 3 x19 x20^2 x22 +

3 x12 x13 x14 x15 x19 x20^2 x22 - 14 x12^2 x15^2 x19 x20^2 x22 -

6 x12 x13 x15^2 x19 x20^2 x22 + 9 x12 x14 x15^2 x19 x20^2 x22 +

3 x13 x14 x15^2 x19 x20^2 x22 - x12^2 x22^2 + x12 x14 x22^2 +

x13 x14 x22^2 - 12 x10 x15 x22^2 + 10 x11 x15 x22^2 +

15 x12 x15 x22^2 + 17 x13 x15 x22^2 + x14 x15 x22^2 -

22 x15^2 x22^2 - 12 x10 x19 x22^2 - 8 x11 x19 x22^2 -

3 x12 x19 x22^2 + x13 x19 x22^2 - 6 x14 x19 x22^2 -

7 x15 x19 x22^2 + 3 x12 x13 x14 x15^2 x19 x22^2 -

12 x10 x20 x22^2 - 6 x11 x20 x22^2 + x12 x20 x22^2 +

2 x13 x20 x22^2 - 7 x14 x20 x22^2 - 18 x15 x20 x22^2 +

4 x12 x13 x14 x15^2 x20 x22^2 - 12 x19 x20 x22^2 +

6 x12 x13 x14 x15 x19 x20 x22^2 - 13 x12^2 x15^2 x19 x20 x22^2 -

12 x12 x13 x15^2 x19 x20 x22^2 + 3 x12 x14 x15^2 x19 x20 x22^2 +

6 x13 x14 x15^2 x19 x20 x22^2 - 6 x20^2 x22^2 +

x12 x13 x14 x15 x20^2 x22^2 - 2 x12 x13 x15^2 x20^2 x22^2 -

2 x12 x14 x15^2 x20^2 x22^2 + x13 x14 x15^2 x20^2 x22^2 +

3 x12 x13 x14 x19 x20^2 x22^2 + 2 x12^2 x15 x19 x20^2 x22^2 -

3 x12 x13 x15 x19 x20^2 x22^2 - 3 x12 x14 x15 x19 x20^2 x22^2 +

3 x13 x14 x15 x19 x20^2 x22^2 - 12 x11 x15^2 x19 x20^2 x22^2 -

8 x12 x15^2 x19 x20^2 x22^2 - 15 x13 x15^2 x19 x20^2 x22^2 -

3 x14 x15^2 x19 x20^2 x22^2 + 12 x10 x22^3 + 12 x11 x22^3 +

x13 x22^3 - 5 x14 x22^3 - 7 x15 x22^3 +

3 x12 x13 x14 x15^2 x22^3 + 2 x19 x22^3 +

9 x12 x13 x14 x15 x19 x22^3 - 9 x12^2 x15^2 x19 x22^3 -

9 x12 x13 x15^2 x19 x22^3 - 3 x12 x14 x15^2 x19 x22^3 +

5 x20 x22^3 + 2 x12 x13 x14 x15 x20 x22^3 +

9 x12^2 x15^2 x20 x22^3 - x12 x13 x15^2 x20 x22^3 -

4 x12 x14 x15^2 x20 x22^3 - x13 x14 x15^2 x20 x22^3 +

3 x12 x13 x14 x19 x20 x22^3 - 2 x12^2 x15 x19 x20 x22^3 -

6 x12 x13 x15 x19 x20 x22^3 - 6 x12 x14 x15 x19 x20 x22^3 -

24 x11 x15^2 x19 x20 x22^3 - 10 x12 x15^2 x19 x20 x22^3 -

21 x13 x15^2 x19 x20 x22^3 - 6 x14 x15^2 x19 x20 x22^3 +

6 x12^2 x15 x20^2 x22^3 - x12 x13 x15 x20^2 x22^3 -

x12 x14 x15 x20^2 x22^3 - x13 x14 x15 x20^2 x22^3 -

12 x11 x15^2 x20^2 x22^3 - 16 x12 x15^2 x20^2 x22^3 -

10 x13 x15^2 x20^2 x22^3 - x14 x15^2 x20^2 x22^3 -

3 x12 x14 x19 x20^2 x22^3 - 3 x13 x14 x19 x20^2 x22^3 -

12 x11 x15 x19 x20^2 x22^3 - x12 x15 x19 x20^2 x22^3 -

9 x13 x15 x19 x20^2 x22^3 - 3 x14 x15 x19 x20^2 x22^3 +

7 x15^2 x19 x20^2 x22^3 + 4 x12 x13 x14 x7 - 4 x14 x15^2 x7 -

4 x13 x14 x19 x7 + 4 x13 x15 x19 x7 + 4 x14 x15 x19 x7 -

4 x15^2 x19 x7 - 4 x12 x13 x20 x7 + 8 x13 x15 x20 x7 -

4 x15^2 x20 x7 + 4 x13 x20^2 x7 - 4 x15 x20^2 x7 -

4 x12 x14 x22 x7 + 4 x13 x15 x22 x7 + 4 x14 x15 x22 x7 -

4 x15^2 x22 x7 + 4 x12 x20 x22 x7 + 4 x13 x20 x22 x7 -

8 x15 x20 x22 x7 + 4 x13 x22^2 x7 - 4 x15 x22^2 x7 +

3 x12 x13 x14 x9 - 4 x12^2 x15 x9 - 2 x12 x13 x15 x9 +

2 x12 x14 x15 x9 + 4 x13 x14 x15 x9 - 2 x11 x15^2 x9 -

x12 x15^2 x9 - 3 x13 x15^2 x9 - 3 x14 x15^2 x9 - 2 x12^2 x19 x9 -

x12 x13 x19 x9 + x12 x14 x19 x9 - x13 x14 x19 x9 +

8 x11 x15 x19 x9 + 4 x12 x15 x19 x9 + 10 x13 x15 x19 x9 +

6 x14 x15 x19 x9 - 9 x15^2 x19 x9 - 3 x12^2 x20 x9 -

3 x12 x13 x20 x9 + 3 x13 x14 x20 x9 + 2 x11 x15 x20 x9 +

4 x12 x15 x20 x9 + 6 x13 x15 x20 x9 - 9 x15^2 x20 x9 +

4 x11 x19 x20 x9 + 2 x12 x19 x20 x9 + x13 x19 x20 x9 -

4 x15 x19 x20 x9 + 3 x12 x13 x14 x15^2 x19 x20 x9 + x13 x20^2 x9 -

12 x15 x20^2 x9 + 3 x12 x13 x14 x15^2 x20^2 x9 - x19 x20^2 x9 -

3 x12^2 x15^2 x19 x20^2 x9 - 3 x12 x13 x15^2 x19 x20^2 x9 +

3 x13 x14 x15^2 x19 x20^2 x9 - 3 x12 x14 x22 x9 +

2 x12 x15 x22 x9 + 4 x13 x15 x22 x9 - 3 x15^2 x22 x9 -

4 x11 x19 x22 x9 - x12 x19 x22 x9 - 4 x13 x19 x22 x9 -

3 x14 x19 x22 x9 - 6 x15 x19 x22 x9 - 4 x11 x20 x22 x9 +

x12 x20 x22 x9 - 3 x14 x20 x22 x9 - 12 x15 x20 x22 x9 -

4 x19 x20 x22 x9 + 3 x12^2 x15^2 x19 x20 x22 x9 -

3 x12 x14 x15^2 x19 x20 x22 x9 + 2 x20^2 x22 x9 -

2 x12 x13 x14 x15 x20^2 x22 x9 + 5 x12^2 x15^2 x20^2 x22 x9 +

3 x12 x13 x15^2 x20^2 x22 x9 - 3 x12 x14 x15^2 x20^2 x22 x9 -

x13 x14 x15^2 x20^2 x22 x9 - x12 x13 x14 x19 x20^2 x22 x9 -

2 x13 x14 x15 x19 x20^2 x22 x9 - 8 x11 x15^2 x19 x20^2 x22 x9 -

5 x12 x15^2 x19 x20^2 x22 x9 - 5 x13 x15^2 x19 x20^2 x22 x9 -

3 x14 x15^2 x19 x20^2 x22 x9 - 4 x11 x22^2 x9 - 2 x12 x22^2 x9 -

12 x15 x22^2 x9 - x20 x22^2 x9 - 2 x12 x13 x14 x15 x20 x22^2 x9 +

5 x12^2 x15^2 x20 x22^2 x9 + 3 x12 x13 x15^2 x20 x22^2 x9 -

x13 x14 x15^2 x20 x22^2 x9 - x12 x13 x14 x19 x20 x22^2 x9 -

2 x13 x14 x15 x19 x20 x22^2 x9 - 2 x11 x15^2 x19 x20 x22^2 x9 -

2 x12 x15^2 x19 x20 x22^2 x9 + x13 x15^2 x19 x20 x22^2 x9 +

2 x12 x14 x15 x20^2 x22^2 x9 - 3 x12 x15^2 x20^2 x22^2 x9 +

x14 x15^2 x20^2 x22^2 x9 - x12^2 x19 x20^2 x22^2 x9 +

x12 x14 x19 x20^2 x22^2 x9 + 2 x11 x15 x19 x20^2 x22^2 x9 +

2 x13 x15 x19 x20^2 x22^2 x9 + 2 x14 x15 x19 x20^2 x22^2 x9 +

2 x15^2 x19 x20^2 x22^2 x9 + 6 x22^3 x9 -

2 x12 x13 x14 x15 x22^3 x9 + 2 x12^2 x15^2 x22^3 x9 +

3 x12 x13 x15^2 x22^3 x9 - x13 x14 x15^2 x22^3 x9 -

x12 x13 x14 x19 x22^3 x9 - 2 x13 x14 x15 x19 x22^3 x9 -

2 x11 x15^2 x19 x22^3 x9 - 2 x12 x15^2 x19 x22^3 x9 +

x13 x15^2 x19 x22^3 x9 + 2 x12 x14 x15 x20 x22^3 x9 +

6 x11 x15^2 x20 x22^3 x9 + 3 x12 x15^2 x20 x22^3 x9 +

6 x13 x15^2 x20 x22^3 x9 + x14 x15^2 x20 x22^3 x9 -

x12^2 x19 x20 x22^3 x9 + x12 x14 x19 x20 x22^3 x9 +

2 x11 x15 x19 x20 x22^3 x9 + 2 x13 x15 x19 x20 x22^3 x9 +

2 x14 x15 x19 x20 x22^3 x9 + 2 x15^2 x19 x20 x22^3 x9 -

x12^2 x20^2 x22^3 x9 + 2 x11 x15 x20^2 x22^3 x9 +

2 x13 x15 x20^2 x22^3 x9 +

5 x15^2 x20^2 x22^3 x9, -2 x12 x13 x14 + 9 x12^2 x15 +

3 x12 x13 x15 - 3 x12 x14 x15 - 5 x13 x14 x15 + 9 x11 x15^2 +

3 x12 x15^2 + 5 x13 x15^2 + 6 x12^2 x19 + 3 x12 x13 x19 -

3 x12 x14 x19 - 2 x13 x14 x19 + 12 x10 x15 x19 - 4 x11 x15 x19 -

9 x12 x15 x19 - 9 x13 x15 x19 - 3 x14 x15 x19 + 23 x15^2 x19 +

5 x12^2 x20 + 2 x12 x13 x20 - 3 x13 x14 x20 + 4 x10 x15 x20 +

2 x11 x15 x20 - 6 x12 x15 x20 - x13 x15 x20 + 16 x15^2 x20 -

5 x11 x19 x20 - 2 x12 x19 x20 + x13 x19 x20 + 15 x15 x19 x20 -

6 x12 x13 x14 x15^2 x19 x20 - 4 x10 x20^2 - 2 x11 x20^2 +

4 x12 x20^2 + 5 x13 x20^2 + 10 x15 x20^2 -

3 x12 x13 x14 x15^2 x20^2 + x19 x20^2 -

3 x12 x13 x14 x15 x19 x20^2 + 6 x12^2 x15^2 x19 x20^2 +

6 x12 x13 x15^2 x19 x20^2 - 3 x13 x14 x15^2 x19 x20^2 +

2 x12 x14 x22 - 3 x12 x15 x22 + 5 x14 x15 x22 - 12 x10 x19 x22 -

7 x11 x19 x22 + 3 x12 x19 x22 + 5 x13 x19 x22 + 2 x14 x19 x22 -

2 x15 x19 x22 - 12 x10 x20 x22 - 7 x11 x20 x22 + 4 x12 x20 x22 +

5 x13 x20 x22 + 3 x14 x20 x22 - 4 x15 x20 x22 - 7 x19 x20 x22 -

6 x12^2 x15^2 x19 x20 x22 + 6 x12 x14 x15^2 x19 x20 x22 -

6 x20^2 x22 + 3 x12 x13 x14 x15 x20^2 x22 -

6 x12^2 x15^2 x20^2 x22 - 3 x12 x13 x15^2 x20^2 x22 +

3 x12 x14 x15^2 x20^2 x22 + 3 x12 x13 x14 x19 x20^2 x22 -

6 x12^2 x15 x19 x20^2 x22 - 3 x12 x13 x15 x19 x20^2 x22 +

3 x12 x14 x15 x19 x20^2 x22 + 3 x13 x14 x15 x19 x20^2 x22 +

6 x11 x15^2 x19 x20^2 x22 + 6 x12 x15^2 x19 x20^2 x22 +

3 x13 x15^2 x19 x20^2 x22 + 3 x14 x15^2 x19 x20^2 x22 -

12 x10 x22^2 - 7 x11 x22^2 + 6 x12 x22^2 + 5 x13 x22^2 +

x15 x22^2 - 3 x20 x22^2 + 3 x12 x13 x14 x15 x20 x22^2 -

6 x12^2 x15^2 x20 x22^2 - 3 x12 x13 x15^2 x20 x22^2 +

3 x12 x13 x14 x19 x20 x22^2 - 3 x12^2 x15 x19 x20 x22^2 -

3 x12 x13 x15 x19 x20 x22^2 + 3 x13 x14 x15 x19 x20 x22^2 -

3 x11 x15^2 x19 x20 x22^2 - 6 x13 x15^2 x19 x20 x22^2 -

3 x12 x14 x15 x20^2 x22^2 + 3 x12 x15^2 x20^2 x22^2 +

3 x12^2 x19 x20^2 x22^2 - 3 x12 x14 x19 x20^2 x22^2 -

6 x11 x15 x19 x20^2 x22^2 - 3 x12 x15 x19 x20^2 x22^2 -

6 x13 x15 x19 x20^2 x22^2 - 3 x14 x15 x19 x20^2 x22^2 +

3 x15^2 x19 x20^2 x22^2 + 2 x22^3 + 3 x12 x13 x14 x15 x22^3 -

3 x12 x13 x15^2 x22^3 + 3 x12 x13 x14 x19 x22^3 -

3 x12^2 x15 x19 x22^3 - 3 x12 x13 x15 x19 x22^3 +

3 x13 x14 x15 x19 x22^3 - 3 x11 x15^2 x19 x22^3 -

6 x13 x15^2 x19 x22^3 + 3 x12^2 x15 x20 x22^3 -

3 x12 x14 x15 x20 x22^3 - 9 x11 x15^2 x20 x22^3 -

9 x12 x15^2 x20 x22^3 - 9 x13 x15^2 x20 x22^3 +

3 x12^2 x19 x20 x22^3 - 3 x12 x14 x19 x20 x22^3 -

6 x11 x15 x19 x20 x22^3 - 3 x12 x15 x19 x20 x22^3 -

6 x13 x15 x19 x20 x22^3 - 3 x14 x15 x19 x20 x22^3 +

3 x15^2 x19 x20 x22^3 + 3 x12^2 x20^2 x22^3 -

6 x11 x15 x20^2 x22^3 - 6 x12 x15 x20^2 x22^3 -

6 x13 x15 x20^2 x22^3 + 4 x12^2 x7 + 4 x13 x15 x7 - 4 x15^2 x7 -

4 x12 x19 x7 - 4 x13 x19 x7 + 4 x15 x19 x7 - 4 x12 x20 x7 +

4 x19 x20 x7 - x12 x13 x9 + x12 x14 x9 + 2 x13 x14 x9 +

x12 x15 x9 + 3 x13 x15 x9 + x14 x15 x9 - 6 x15^2 x9 +

6 x11 x19 x9 + x13 x19 x9 + x14 x19 x9 + 5 x15 x19 x9 +

x12 x13 x14 x15^2 x19 x9 + 3 x11 x20 x9 + x13 x20 x9 -

x15 x20 x9 + 2 x12 x13 x14 x15^2 x20 x9 + 2 x19 x20 x9 -

x12 x13 x14 x15 x19 x20 x9 - x12^2 x15^2 x19 x20 x9 -

x12 x13 x15^2 x19 x20 x9 + 2 x13 x14 x15^2 x19 x20 x9 -

4 x20^2 x9 + x12 x13 x14 x15 x20^2 x9 - 2 x12^2 x15^2 x20^2 x9 -

2 x12 x13 x15^2 x20^2 x9 + x13 x14 x15^2 x20^2 x9 +

x12^2 x15 x19 x20^2 x9 + x12 x13 x15 x19 x20^2 x9 +

x13 x14 x15 x19 x20^2 x9 + 3 x11 x15^2 x19 x20^2 x9 +

2 x12 x15^2 x19 x20^2 x9 + x13 x15^2 x19 x20^2 x9 + x12 x22 x9 -

2 x14 x22 x9 + x15 x22 x9 - 5 x19 x22 x9 + x12^2 x15^2 x19 x22 x9 -

x12 x14 x15^2 x19 x22 x9 - 4 x20 x22 x9 +

x12^2 x15^2 x20 x22 x9 - 2 x12 x14 x15^2 x20 x22 x9 -

x12^2 x15 x19 x20 x22 x9 + x12 x14 x15 x19 x20 x22 x9 -

3 x11 x15^2 x19 x20 x22 x9 - x12 x15^2 x19 x20 x22 x9 -

3 x13 x15^2 x19 x20 x22 x9 - 2 x14 x15^2 x19 x20 x22 x9 -

x12 x13 x14 x20^2 x22 x9 + x12^2 x15 x20^2 x22 x9 +

x12 x13 x15 x20^2 x22 x9 - x12 x14 x15 x20^2 x22 x9 -

x13 x14 x15 x20^2 x22 x9 - x11 x15^2 x20^2 x22 x9 -

x14 x15^2 x20^2 x22 x9 - x13 x14 x19 x20^2 x22 x9 -

4 x11 x15 x19 x20^2 x22 x9 - x12 x15 x19 x20^2 x22 x9 -

3 x13 x15 x19 x20^2 x22 x9 - x14 x15 x19 x20^2 x22 x9 -

6 x22^2 x9 + x12^2 x15^2 x22^2 x9 - x12 x13 x14 x20 x22^2 x9 +

x12^2 x15 x20 x22^2 x9 + x12 x13 x15 x20 x22^2 x9 -

x13 x14 x15 x20 x22^2 x9 - x11 x15^2 x20 x22^2 x9 -

2 x12 x15^2 x20 x22^2 x9 - x13 x14 x19 x20 x22^2 x9 -

4 x11 x15 x19 x20 x22^2 x9 - 2 x12 x15 x19 x20 x22^2 x9 -

3 x13 x15 x19 x20 x22^2 x9 + 3 x15^2 x19 x20 x22^2 x9 +

x12 x14 x20^2 x22^2 x9 - x12 x15 x20^2 x22^2 x9 +

x14 x15 x20^2 x22^2 x9 - x15^2 x20^2 x22^2 x9 +

x11 x19 x20^2 x22^2 x9 + x13 x19 x20^2 x22^2 x9 +

x14 x19 x20^2 x22^2 x9 + 4 x15 x19 x20^2 x22^2 x9 -

x12 x13 x14 x22^3 x9 + 2 x12^2 x15 x22^3 x9 +

x12 x13 x15 x22^3 x9 - x13 x14 x15 x22^3 x9 +

2 x11 x15^2 x22^3 x9 + 3 x13 x15^2 x22^3 x9 -

x13 x14 x19 x22^3 x9 - 4 x11 x15 x19 x22^3 x9 -

2 x12 x15 x19 x22^3 x9 - 3 x13 x15 x19 x22^3 x9 +

3 x15^2 x19 x22^3 x9 + x12 x14 x20 x22^3 x9 -

3 x12 x15 x20 x22^3 x9 + x14 x15 x20 x22^3 x9 +

4 x15^2 x20 x22^3 x9 + x11 x19 x20 x22^3 x9 +

x13 x19 x20 x22^3 x9 + x14 x19 x20 x22^3 x9 +

4 x15 x19 x20 x22^3 x9 + x11 x20^2 x22^3 x9 + x13 x20^2 x22^3 x9 +

5 x15 x20^2 x22^3 x9, -x11 x15^2 - 3 x10 x15 x19 - 2 x11 x15 x19 -

3 x15^2 x19 - x10 x15 x20 - 2 x11 x15 x20 - 2 x15^2 x20 +

x11 x19 x20 - 3 x15 x19 x20 + x10 x20^2 + x11 x20^2 - x15 x20^2 +

3 x10 x19 x22 + 3 x11 x19 x22 + 2 x15 x19 x22 + 3 x10 x20 x22 +

3 x11 x20 x22 + 2 x15 x20 x22 + 2 x19 x20 x22 + x20^2 x22 +

3 x10 x22^2 + 3 x11 x22^2 + 2 x15 x22^2 + x20 x22^2 - x22^3 +

x11 x15 x7 + x15^2 x7 - x11 x19 x7 + x15 x20 x7 + x20^2 x7 +

x19 x22 x7 + x20 x22 x7 + x22^2 x7 + x11 x15 x9 + x15^2 x9 -

x11 x19 x9 + x15 x20 x9 + x20^2 x9 + x19 x22 x9 + x20 x22 x9 +

x22^2 x9,

2 x10 x15 + x11 x15 + x15^2 + x11 x19 + x15 x20 - x20^2 - x19 x22 -

x20 x22 - x22^2 + x10 x7 + x11 x7 + x15 x7 + x20 x7 + x10 x9 +

x11 x9 + x15 x9 + x20 x9, -x10 x15 - x15^2 + x10 x20 + x11 x20 +

x20^2 - x15 x7 - x11 x9 + x7 x9,

3 x10 x15 + x11 x15 + 2 x15^2 + 2 x11 x19 + 2 x15 x20 - x20^2 -

2 x19 x22 - 2 x20 x22 - 2 x22^2 + x11 x7 + x15 x7 + x20 x7 -

x11 x8 + x7 x8 + x10 x9 + x11 x9 + x15 x9 + x20 x9, -2 x10 x15 -

x11 x15 - x15^2 - x11 x19 - x10 x20 - 2 x15 x20 + x19 x22 +

x20 x22 + x22^2 - x11 x7 - x20 x7 + x7^2 - x10 x9 - x11 x9 -

x15 x9 - x20 x9,

2 x10 x15 + x11 x15 + 2 x15^2 + x11 x19 + x10 x20 + 2 x15 x20 -

x19 x22 - x20 x22 - x22^2 + x15 x6 + x6^2 + x11 x7 + x15 x7 +

x20 x7 + x6 x7 + x10 x9 + x11 x9 + x15 x9 + x20 x9,

x10 x15 x19 + x11 x15 x19 + x15^2 x19 + x15^2 x20 - x11 x19 x20 +

x15 x19 x20 - x10 x20^2 - x11 x20^2 - x10 x19 x22 - x11 x19 x22 -

x15 x19 x22 - x10 x20 x22 - x11 x20 x22 - x15 x20 x22 - x10 x22^2 -

x11 x22^2 - x15 x22^2 - 2 x10 x15 x5 - x11 x15 x5 - 2 x15^2 x5 -

x11 x19 x5 - x10 x20 x5 - 2 x15 x20 x5 + x19 x22 x5 + x20 x22 x5 +

x22^2 x5 + x5^3 - x15 x5 x6 + x5^2 x6 + x11 x19 x7 - x20^2 x7 -

x19 x22 x7 - x20 x22 x7 - x22^2 x7 - x11 x5 x7 - x15 x5 x7 -

x20 x5 x7 + x15 x6 x7 - x5 x6 x7 + x10 x15 x9 + x11 x19 x9 -

x20^2 x9 - x19 x22 x9 - x20 x22 x9 - x22^2 x9 - x10 x5 x9 -

x11 x5 x9 - x15 x5 x9 - x20 x5 x9, -2 x10 x15 - x11 x15 - x15^2 -

x11 x19 - x10 x20 - 2 x15 x20 + x19 x22 + x20 x22 + x22^2 + x4 x5 +

x5^2 + x5 x6 - x11 x7 - x20 x7 - x4 x7 - x6 x7 - x10 x9 - x11 x9 -

x15 x9 - x20 x9, -x15^2 + x4^2 - x15 x6 + x4 x6 - x15 x7 + x4 x7,

2 x10 x15 + x11 x15 + 2 x15^2 + x11 x19 + x10 x20 + 2 x15 x20 -

x19 x22 - x20 x22 - x22^2 + x3^2 + x3 x4 + x3 x5 + x15 x6 - x4 x6 -

x5 x6 + x11 x7 + x15 x7 + x20 x7 + x6 x7 + x10 x9 + x11 x9 +

x15 x9 + x20 x9, -2 x10 x15 - x11 x15 - 2 x15^2 - x11 x19 + x2^2 -

x10 x20 - 2 x15 x20 + x19 x22 + x20 x22 + x22^2 + x2 x3 - x3 x4 +

x2 x5 + x5^2 - x15 x6 + x4 x6 + x5 x6 - x11 x7 - x15 x7 - x20 x7 -

x6 x7 - x10 x9 - x11 x9 - x15 x9 - x20 x9, -1 + x1^4}}

どわああああああ！！！！！

なんか一気にきたああああああ！！！！！

おいいいいいいいい！！！！！！！

と、なんか銀魂っぽいリアクションをしながら、冷静な南條を見て、我に返る。

「結果。グレブナー基底は {1} ではないので、四色で塗り分け可能であることが分かった。また、計算にかかった時間は、53.511秒。今までのに比べて、結構時間がかかっている。」

「ああ…確かに…」

「では。次に、F_5での計算時間を測ろう。」

「ちょ、ちょっと待ってくれ。」

そんな俺にお構いなしに南條は実行する。

{23.5409, {4 + x22^4, x20^3 + x20^2 x22 + x20 x22^2 + x22^3,

x19^2 + x19 x20 + x20^2 + x19 x22 + x20 x22 + x22^2,

x15^3 + x15^2 x20 + x15 x20^2 + 4 x20^2 x22 + 4 x20 x22^2 + 4 x22^3,

x14^2 + x14 x19 + 4 x19 x20 + 4 x20^2 + x14 x22 + 4 x20 x22,

x13^2 + x13 x14 + x13 x19 + 4 x14 x22 + 4 x19 x22 + 4 x22^2,

x12^2 x14 + x12^2 x19 + 4 x12 x14 x19 + x12^2 x20 + 4 x12 x14 x20 +

4 x12 x19 x20 + x14 x19 x20 + x12^2 x22 + x12 x22^2 + x22^3,

x12^2 x13 + 4 x12 x13 x19 + 4 x12^2 x20 + 4 x12 x13 x20 +

x12 x19 x20 + x13 x19 x20 + x12 x20^2 + 4 x19 x20^2,

x12^3 + 4 x12 x13 x14 + x13 x14 x19 + x12^2 x20 + x12 x13 x20 +

4 x12 x19 x20 + 4 x13 x19 x20 + 4 x12 x20^2 + x19 x20^2 +

x12 x14 x22 + x12 x19 x22 + 4 x14 x19 x22 + x12 x22^2 + x22^3,

x11 x14 + x13 x14 + x11 x19 + x13 x19 + x14 x19 + x11 x20 +

x13 x20 + x14 x20 + x19 x20 + x11 x22 + x13 x22 + 4 x22^2,

x11 x13 + 4 x13 x14 + 4 x11 x20 + 4 x19 x20 + 4 x20^2 + x14 x22 +

x19 x22 + x22^2,

x11 x12 + x12^2 + x12 x13 + 4 x11 x19 + 4 x13 x19 + x19 x20 +

x20^2 + x19 x22 + x20 x22 + x22^2,

x11^2 + x11 x19 + x11 x20 + 4 x19 x22 + 4 x20 x22 + 4 x22^2,

x10 x15^2 + x11 x15^2 + x10 x15 x19 + x11 x15 x19 + x15^2 x19 +

x10 x15 x20 + x11 x15 x20 + x15^2 x20 + x15 x19 x20 +

4 x10 x19 x22 + 4 x11 x19 x22 + 4 x15 x19 x22 + 4 x10 x20 x22 +

4 x11 x20 x22 + 4 x15 x20 x22 + 4 x19 x20 x22 + 4 x10 x22^2 +

4 x11 x22^2 + 4 x15 x22^2 + x22^3,

2 x12 x13 x14 + 2 x12^2 x15 + 4 x12 x13 x15 + x10 x14 x15 +

4 x12 x14 x15 + 3 x13 x14 x15 + 2 x11

***省略***

5 x9 + 4 x20 x9, 4 x15^2 + x4^2 + 4 x15 x6 + x4 x6 + 4 x15 x7 + x4 x7,

2 x10 x15 + x11 x15 + 2 x15^2 + x11 x19 + x10 x20 + 2 x15 x20 +

4 x19 x22 + 4 x20 x22 + 4 x22^2 + x3^2 + x3 x4 + x3 x5 + x15 x6 +

4 x4 x6 + 4 x5 x6 + x11 x7 + x15 x7 + x20 x7 + x6 x7 + x10 x9 +

x11 x9 + x15 x9 + x20 x9,

3 x10 x15 + 4 x11 x15 + 3 x15^2 + 4 x11 x19 + x2^2 + 4 x10 x20 +

3 x15 x20 + x19 x22 + x20 x22 + x22^2 + x2 x3 + 4 x3 x4 + x2 x5 +

x5^2 + 4 x15 x6 + x4 x6 + x5 x6 + 4 x11 x7 + 4 x15 x7 + 4 x20 x7 +

4 x6 x7 + 4 x10 x9 + 4 x11 x9 + 4 x15 x9 + 4 x20 x9, 4 + x1^4}}

しばらくして、Outputが表示された。

体感では、さっきより長かった気がする。

「結果。計算時間は、23.5409秒。さっきの53.511秒に比べて、３０秒ほど早くなっている。」

「おおー！」

「結論。これで、このケースにおいて、"有限体の方が有理数体よりグレブナー基底の計算時間が早くなる"という仮説は、実験により検証された。」

「おお……つまり、四色で塗り分けできるか判定するときは、複素数で考えるより、F_5で考えた方が、効率的ってことか……勉強になった……」

ふう。

色々大変だったが、これで、南條も満足してくれただろう。

ようやく、導来圏にどう立ち向かうかの対策を……

「では。次に西日本も含めて計算してみよう。」

「え…」

「疑問。有限体でもどのくらい時間がかかるのか、とても気になるだろう。」

「え、あ、う。」

「そのために。本条は早く、西日本の多項式を書き下してくれ。」

なんてこった。パンナコッタ。

くっ……こんなことなら、Case. 2 にしておけばよかった…

神め……。選択を誤りやがって…

お冷の氷がすっかり溶けて、カランと音がなる。

こうして、終わらない計算とともに、長い夜は更けていくのであった。

作者を応援しよう！

ハートをクリックで、簡単に応援の気持ちを伝えられます。（ログインが必要です）

応援したユーザー

新規登録で充実の読書を

マイページ: 読書の状況から作品を自動で分類して簡単に管理できる; 小説の未読話数がひと目でわかり前回の続きから読める; フォローしたユーザーの活動を追える
通知: 小説の更新や作者の新作の情報を受け取れる
閲覧履歴: 以前読んだ小説が一覧で見つけやすい

カクヨムで可能な読書体験をくわしく知る

次のエピソード Case. 2

作者を応援しよう！

応援したユーザー

応援すると応援コメントも書けます

新規登録で充実の読書を

文字サイズ

背景色

フォント

組み方向

応援の気持ちを届けよう

フォロー機能を活用しよう

フォロー機能を活用しよう