Case 1

원문

 ".......하지만 여기에 무슨 장점이 있는 거지?"

 나는 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같은 걸 쓰면 되나?"
 "적절."

 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]

 아까 입력한 식의 맨 마지막 부분에 "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의 대수적 폐포(algebraic closure)를 생각하면, 복소수일 때와 비슷하게 힐베르트 영점 정리를 쓸 수 있으니 방금 계산한 그뢰브너 기저에 {1}이 없다는 사실로부터 도쿄, 치바, 카나가와, 사이타마, 야마나시, 시즈오카, 나가노를 네 색깔로 구분할 수 있다는 것을 알 수 있어."

 "그래도 이거 유리수일 때랑 비교해도 식이 썩 간단하진 않은 거 같은데?"

 "동의. 별 차이 없는 것 같아."

 "그럼 mod 5로 계산해도 별 의미 없는 건가?"
 "조급. 출력된 결과는 별 차이 없다고 해도, 계산시간이 더 빨라졌을 지도 몰라. Timing을 써서 재 보자."

 난죠는 Mathematica에 Timing이라고 타이핑했다.

 "이름대로. 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}]]

 "우선 characteristic 0, 즉 유리수 체인 경우부터 해볼게."

 "다시 말해서 복소수에서 연립방정식을 풀겠다는 거구만."

 {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초로, 정말 근소해. 좀 더 큰 연립방정식에서도 유의미한 차이가 나는 지 검증할 필요가 있을 것 같아."
 "오오─ 뭔가 실험수학같은 느낌인데."

 "정의. 실험수학을 어떻게 정의하냐에 따라 다르겠지만, '유한체에서 계산하면 더 빨리 끝난다'는 가설을 실험으로 검증하려 하는 거니 그리 말하는 것도 무리는 아니겠지."

 실험이라는 단어는 그 말에서 느껴지는 이미지 때문에 물리나 화학같은 분야에서만 사용될 것 같다는 인상이 있지만, 컴퓨터를 사용하는 수학에서도 쓰는 때가 있다.

 손계산 대신 컴퓨터를 써서 예측을 증명하는 게 실험이랑 비슷해 보여서 그렇게 부르는 것이리라.

 "예시. 차이가 나는 지 검증하기 위해서는 더 많은 다항식이 필요해."

 "음. 그러겠네."
 "시험삼아. 일본 전도를 다항식으로 표현해보자."

 "뭐!?"
 "의문. 안 돼?"

 일본에 얼마나 많은 행정구역이 있는지 생각했다. 47개다.

 도 1개에 현 6개만 가져와도 식 17개짜리 연립방정식이 나오는데, 전국 지도를 가져오면 식이 몇 개나 나올런지.

 애당초 그걸 다 쓰는 것 자체가 귀찮은, 아니, 힘든 일이다.

 "그럼. 나는 동일본을 할 테니까 너는 서일본을 맡아줘."

 난죠는 그렇게 말하더니 다항식을 술술 타이핑하기 시작했다.

 이럴 때 난죠의 집중력은 대단한지라 무슨 말을 해도 듣지 않는다.

 별 수 없지. 하는 수밖에 없다.

 야심한 시간의 패밀리 레스토랑에 난죠의 키보드 소리와 내가 종이에 다항식을 끄적이는 소리가 퍼진다.

 둘이 함께 이러고 있으니 옛날에 같이 과제를 했던 시절이 떠오른다.

 난죠가 안색 하나 변함 없이 손을 놀린다.

 그 눈빛 깊이 서린 열정이 내게도 전해져 온다.

 이런저런 일이 있긴 했어도 난죠가 내 친구라는 사실이 마음에 든다.

 "완료. 작업 완료했어"

 내가 시코쿠도 끝내지 못한 와중에 난죠가 고개를 들며 말했다.

 "뭐야, 벌써 끝났어!?"

 "YES. 끝났어."

 "빠르네..."

 "거꾸로. 너는 아직 안 끝났, 어?"

 나는 난죠처럼 대단한 스펙같은 건 갖고 있지 않다.

 수험생 시절애 센터 시험을 90%나 맞춘 것도 운이나 다름없었다.

 "그럼. 우선 동일본만이라도 그뢰브너 기저를 계산해보지."

 난죠가 모니터를 내 쪽으로 돌렸다.

 행정구역들로 된 다항식이 줄줄이 입력되어 있었다.

 홋카이도 ↔︎ 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

 "일단. 동일본의 열여덟 행정구역에 대해 변수 18개를 대응시켰어. 변수의 첨수는 총무성이 각 행정구역에 부여한 코드 번호를 참고했어. 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에서 그뢰브너 기저를 계산하는 데 걸리는 시간을 재보자."

 "자, 잠깐만."

 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}, Modulus->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초에 비하면 30초 정도 빠르네."

 "오오─!"

 "결론. 이로써 이 케이스에 대해서 '유한체가 유리수보다 그뢰브너 계산 속도가 빠르다'는 가설이 실험적으로 검증되었어."

 "오오......그러니까 네 색으로 지도를 잘 칠할 수 있는지 판정할 때 복소수보다는 F_5를 생각하는 게 더 효율적이라는 거지...... 좋은 거 배웠네......"

 후우.

 이래저래 힘들었지만 이걸로 난죠도 만족했겠지.

 드디어 도라이 켄을 어떻게 상대해야 할 지 대책을...

 "그럼. 다음으로 서일본도 넣어서 계산해보자."

 "아니..."

 "의문. 유한체에선 시간이 얼마나 걸릴 지 정말 궁금하지 않아?"

 "...."
 "그러니. 혼죠, 서일본쪽 다항식을 처음부터 다시 써 줘."

 않이 외죠.

 으윽......이럴 줄 알았으면 Case 2라고 할 걸 그랬어......

 하나님 이 녀석...... 좀 제대로 고를 것이지...... 

 물 안에 들어있던 얼음이 녹으며 쩍 갈라지는 소리를 낸다.

 이리하여 끝없는 계산과 함께 길고 긴 밤이 깊어가고 있었다.