include("amalgamation.jl");

Example 3.3

The two representations of \(S^1\) that we want to amalgamate are \(v=(1,0,-1)\) and \(w=(1,1,-2)\). We use the first 4 Schur polynomials, i.e., \(s_{1,1,1}, s_1,s_{1,1}\), and \(s_2\).

v = [-1,0,1];
w = [-2,1,1];
k = 4;

We are interested in finding a concrete amalgamation, so we set up the integer linear program \(\mathrm{ILP}_k\) using the following command:

lp(k,v,w;integer=false, upper_bound=10000)

In the case of integer=true, an artificial upper bound is given, because solve_milp requires a bounded polytope.

m = lp(k,v,w;integer=true);

We use the OSCAR command solve_milp to solve \(\mathrm{ILP}_k\). We display the solution with display_solution. It shows the solutions in a few ways: - \(P\) and \(Q\) as a symmetric polynomials written in terms of the Schur polynomials. - \(P\) and \(Q\) as a polynomials in three variables \(x_1,x_2,x_3\) - \(P_v(z)\) and equivalently, \(Q_w(z)\), as a Laurent polynomial in \(z\)

_, sol = solve_milp(m);
display_solution(sol,k,v,w);

In the Schur basis, P = s_[1] + s_[2]
==================
In the Schur basis, Q = 3s_[1, 1, 1] + s_[1] + s_[1, 1]
==================
P = dot_prod(sol_v, list_s) = x1^2 + x1*x2 + x1*x3 + x1 + x2^2 + x2*x3 + x2 + x3^2 + x3
==================
Q = dot_prod(sol_w, list_s) = 3*x1*x2*x3 + x1*x2 + x1*x3 + x1 + x2*x3 + x2 + x3
==================
dimension is P(1, 1, 1) = 9
==================
Pz = P(z ^ v[1], z ^ v[2], z ^ v[3]) = z^2 + 2*z + 3 + 2*z^-1 + z^-2

We verify the solution by plugging in \(P_v=P(z^{v[1]},z^{v[2]},z^{v[3]})\) and \(Q_w=Q(z^{w[1]},z^{w[2]},z^{w[3]})\), and checking that they are equal. We also verify that they represent injective representations by checking \(P(\xi,\xi,\xi) \neq P(1,1,1)\) and \(Q(\xi,\xi,\xi) \neq Q(1,1,1)\), where \(\xi\) is a third root of unity.

verify_solution(sol,k,v,w);

dimension P(1, 1, 1) = 9
Pv == Qw = true
check 3rd root of unity P(xi, xi, xi) == P(1, 1, 1) = false
Q(xi, xi, xi) == Q(1, 1, 1) = false

Producing Table 1

Entries in Table 1 are found using the following command:

find_min_k(max_k,v,w; using_scip=false, min_k=1)

This function solves for the feasibility of the linear relaxation of \(\mathrm{ILP}_k\). For \(k\) values less than 150, set using_scip=false; for \(k\) values at least 150, we reccommend setting using_scip=true. Note that if you set using_scip=true, the program will produce .lp files that are saved in the same folder as this notebook.

v = [1,5,-6]
w = [1,7,-8]
find_min_k(150,v,w;using_scip=false);

k = 75
k = 113
k = 132
k = 122
k = 117
k = 119
k = 120
minimal k is 120

In some cases, no solution is found given the max \(k\) value.

v = [1,2,-3]
w = [1,3,-4]
find_min_k(20,v,w;using_scip=false);

no solution found

In this case, double the max \(k\) value and set the min \(k\) value to be the previous max value.

v = [1,2,-3]
w = [1,3,-4]
find_min_k(40,v,w;using_scip=false,min_k=20);

k = 30
k = 24
k = 21
k = 20
minimal k is 21

Producing Table 2

Given a pair of vectors \(v\) and \(w\), and their minimal \(k\) value from Table 1, we solve \(\mathrm{ILP}_k\). For \(k<100\), use solve_milp; for \(k\geq 100\), we recommend saving the ILP as an .lp file and solving it using SCIP.

v = [1,6,-7];
w = [1,7,-8];
k = 87;
m = lp(k,v,w;integer=true);
_, sol = solve_milp(m);
display_solution(sol,k,v,w);

In the Schur basis, P = 16s_{1} + 16s_{1, 1} + 6s_{2} + 32s_{2, 1} + 6s_{2, 2} + s_{3} + 11s_{3, 1} + 11s_{3, 2} + s_{3, 3} + 23s_{4} + 14s_{4, 1} + 8s_{4, 2} + 14s_{4, 3} + 23s_{4, 4} + 15s_{5, 1} + 7s_{5, 2} + 7s_{5, 3} + 15s_{5, 4} + 8s_{6} + 9s_{6, 1} + 42s_{6, 2} + 32s_{6, 3} + 42s_{6, 4} + 9s_{6, 5} + 8s_{6, 6} + 30s_{7} + 2s_{7, 1} + 10s_{7, 2} + 27s_{7, 3} + 27s_{7, 4} + 10s_{7, 5} + 2s_{7, 6} + 30s_{7, 7} + 25s_{8} + 15s_{8, 1} + 3s_{8, 2} + 18s_{8, 3} + 37s_{8, 4} + 18s_{8, 5} + 3s_{8, 6} + 15s_{8, 7} + 25s_{8, 8} + 7s_{9, 1} + s_{9, 2} + 12s_{9, 3} + 25s_{9, 4} + 25s_{9, 5} + 12s_{9, 6} + s_{9, 7} + 7s_{9, 8} + 24s_{10} + 7s_{10, 1} + 21s_{10, 2} + 9s_{10, 3} + 17s_{10, 4} + 22s_{10, 5} + 17s_{10, 6} + 9s_{10, 7} + 21s_{10, 8} + 7s_{10, 9} + 24s_{10, 10} + 11s_{11} + 13s_{11, 1} + 6s_{11, 2} + 28s_{11, 3} + 12s_{11, 4} + 8s_{11, 5} + 8s_{11, 6} + 12s_{11, 7} + 28s_{11, 8} + 6s_{11, 9} + 13s_{11, 10} + 11s_{11, 11} + 21s_{12, 4} + 6s_{12, 5} + 11s_{12, 6} + 6s_{12, 7} + 21s_{12, 8}
==================
In the Schur basis, Q = 43s_{1, 1, 1} + 3s_{1} + 3s_{1, 1} + 10s_{2} + 19s_{2, 1} + 10s_{2, 2} + 36s_{3} + 42s_{3, 1} + 42s_{3, 2} + 36s_{3, 3} + 43s_{4} + 18s_{4, 1} + 25s_{4, 2} + 18s_{4, 3} + 43s_{4, 4} + 49s_{5} + 20s_{5, 1} + 51s_{5, 2} + 51s_{5, 3} + 20s_{5, 4} + 49s_{5, 5} + 57s_{6} + 16s_{6, 1} + 43s_{6, 2} + 71s_{6, 3} + 43s_{6, 4} + 16s_{6, 5} + 57s_{6, 6} + 39s_{7} + 13s_{7, 2} + 25s_{7, 3} + 25s_{7, 4} + 13s_{7, 5} + 39s_{7, 7} + 37s_{8} + 7s_{8, 1} + 33s_{8, 2} + 48s_{8, 3} + 26s_{8, 4} + 48s_{8, 5} + 33s_{8, 6} + 7s_{8, 7} + 37s_{8, 8} + 13s_{9} + 4s_{9, 1} + 13s_{9, 2} + 48s_{9, 3} + 33s_{9, 4} + 33s_{9, 5} + 48s_{9, 6} + 13s_{9, 7} + 4s_{9, 8} + 13s_{9, 9} + 21s_{10} + 6s_{10, 1} + 11s_{10, 2} + 17s_{10, 3} + 34s_{10, 4} + 27s_{10, 5} + 34s_{10, 6} + 17s_{10, 7} + 11s_{10, 8} + 6s_{10, 9} + 21s_{10, 10}
==================
P = dot_prod(sol_v, list_s) = 21*x1^12*x2^8 + 21*x1^12*x2^7*x3 + 6*x1^12*x2^7 + 21*x1^12*x2^6*x3^2 + 6*x1^12*x2^6*x3 + 11*x1^12*x2^6 + 21*x1^12*x2^5*x3^3 + 6*x1^12*x2^5*x3^2 + 11*x1^12*x2^5*x3 + 6*x1^12*x2^5 + 21*x1^12*x2^4*x3^4 + 6*x1^12*x2^4*x3^3 + 11*x1^12*x2^4*x3^2 + 6*x1^12*x2^4*x3 + 21*x1^12*x2^4 + 21*x1^12*x2^3*x3^5 + 6*x1^12*x2^3*x3^4 + 11*x1^12*x2^3*x3^3 + 6*x1^12*x2^3*x3^2 + 21*x1^12*x2^3*x3 + 21*x1^12*x2^2*x3^6 + 6*x1^12*x2^2*x3^5 + 11*x1^12*x2^2*x3^4 + 6*x1^12*x2^2*x3^3 + 21*x1^12*x2^2*x3^2 + 21*x1^12*x2*x3^7 + 6*x1^12*x2*x3^6 + 11*x1^12*x2*x3^5 + 6*x1^12*x2*x3^4 + 21*x1^12*x2*x3^3 + 21*x1^12*x3^8 + 6*x1^12*x3^7 + 11*x1^12*x3^6 + 6*x1^12*x3^5 + 21*x1^12*x3^4 + 11*x1^11*x2^11 + 11*x1^11*x2^10*x3 + 13*x1^11*x2^10 + 11*x1^11*x2^9*x3^2 + 13*x1^11*x2^9*x3 + 27*x1^11*x2^9 + 11*x1^11*x2^8*x3^3 + 13*x1^11*x2^8*x3^2 + 48*x1^11*x2^8*x3 + 34*x1^11*x2^8 + 11*x1^11*x2^7*x3^4 + 13*x1^11*x2^7*x3^3 + 48*x1^11*x2^7*x3^2 + 40*x1^11*x2^7*x3 + 23*x1^11*x2^7 + 11*x1^11*x2^6*x3^5 + 13*x1^11*x2^6*x3^4 + 48*x1^11*x2^6*x3^3 + 40*x1^11*x2^6*x3^2 + 34*x1^11*x2^6*x3 + 14*x1^11*x2^6 + 11*x1^11*x2^5*x3^6 + 13*x1^11*x2^5*x3^5 + 48*x1^11*x2^5*x3^4 + 40*x1^11*x2^5*x3^3 + 34*x1^11*x2^5*x3^2 + 20*x1^11*x2^5*x3 + 29*x1^11*x2^5 + 11*x1^11*x2^4*x3^7 + 13*x1^11*x2^4*x3^6 + 48*x1^11*x2^4*x3^5 + 40*x1^11*x2^4*x3^4 + 34*x1^11*x2^4*x3^3 + 20*x1^11*x2^4*x3^2 + 50*x1^11*x2^4*x3 + 12*x1^11*x2^4 + 11*x1^11*x2^3*x3^8 + 13*x1^11*x2^3*x3^7 + 48*x1^11*x2^3*x3^6 + 40*x1^11*x2^3*x3^5 + 34*x1^11*x2^3*x3^4 + 20*x1^11*x2^3*x3^3 + 50*x1^11*x2^3*x3^2 + 12*x1^11*x2^3*x3 + 28*x1^11*x2^3 + 11*x1^11*x2^2*x3^9 + 13*x1^11*x2^2*x3^8 + 48*x1^11*x2^2*x3^7 + 40*x1^11*x2^2*x3^6 + 34*x1^11*x2^2*x3^5 + 20*x1^11*x2^2*x3^4 + 50*x1^11*x2^2*x3^3 + 12*x1^11*x2^2*x3^2 + 28*x1^11*x2^2*x3 + 6*x1^11*x2^2 + 11*x1^11*x2*x3^10 + 13*x1^11*x2*x3^9 + 48*x1^11*x2*x3^8 + 40*x1^11*x2*x3^7 + 34*x1^11*x2*x3^6 + 20*x1^11*x2*x3^5 + 50*x1^11*x2*x3^4 + 12*x1^11*x2*x3^3 + 28*x1^11*x2*x3^2 + 6*x1^11*x2*x3 + 13*x1^11*x2 + 11*x1^11*x3^11 + 13*x1^11*x3^10 + 27*x1^11*x3^9 + 34*x1^11*x3^8 + 23*x1^11*x3^7 + 14*x1^11*x3^6 + 29*x1^11*x3^5 + 12*x1^11*x3^4 + 28*x1^11*x3^3 + 6*x1^11*x3^2 + 13*x1^11*x3 + 11*x1^11 + 11*x1^10*x2^11*x3 + 13*x1^10*x2^11 + 11*x1^10*x2^10*x3^2 + 26*x1^10*x2^10*x3 + 51*x1^10*x2^10 + 11*x1^10*x2^9*x3^3 + 26*x1^10*x2^9*x3^2 + 78*x1^10*x2^9*x3 + 41*x1^10*x2^9 + 11*x1^10*x2^8*x3^4 + 26*x1^10*x2^8*x3^3 + 99*x1^10*x2^8*x3^2 + 75*x1^10*x2^8*x3 + 44*x1^10*x2^8 + 11*x1^10*x2^7*x3^5 + 26*x1^10*x2^7*x3^4 + 99*x1^10*x2^7*x3^3 + 81*x1^10*x2^7*x3^2 + 67*x1^10*x2^7*x3 + 23*x1^10*x2^7 + 11*x1^10*x2^6*x3^6 + 26*x1^10*x2^6*x3^5 + 99*x1^10*x2^6*x3^4 + 81*x1^10*x2^6*x3^3 + 78*x1^10*x2^6*x3^2 + 37*x1^10*x2^6*x3 + 46*x1^10*x2^6 + 11*x1^10*x2^5*x3^7 + 26*x1^10*x2^5*x3^6 + 99*x1^10*x2^5*x3^5 + 81*x1^10*x2^5*x3^4 + 78*x1^10*x2^5*x3^3 + 43*x1^10*x2^5*x3^2 + 75*x1^10*x2^5*x3 + 34*x1^10*x2^5 + 11*x1^10*x2^4*x3^8 + 26*x1^10*x2^4*x3^7 + 99*x1^10*x2^4*x3^6 + 81*x1^10*x2^4*x3^5 + 78*x1^10*x2^4*x3^4 + 43*x1^10*x2^4*x3^3 + 96*x1^10*x2^4*x3^2 + 46*x1^10*x2^4*x3 + 45*x1^10*x2^4 + 11*x1^10*x2^3*x3^9 + 26*x1^10*x2^3*x3^8 + 99*x1^10*x2^3*x3^7 + 81*x1^10*x2^3*x3^6 + 78*x1^10*x2^3*x3^5 + 43*x1^10*x2^3*x3^4 + 96*x1^10*x2^3*x3^3 + 46*x1^10*x2^3*x3^2 + 73*x1^10*x2^3*x3 + 15*x1^10*x2^3 + 11*x1^10*x2^2*x3^10 + 26*x1^10*x2^2*x3^9 + 99*x1^10*x2^2*x3^8 + 81*x1^10*x2^2*x3^7 + 78*x1^10*x2^2*x3^6 + 43*x1^10*x2^2*x3^5 + 96*x1^10*x2^2*x3^4 + 46*x1^10*x2^2*x3^3 + 73*x1^10*x2^2*x3^2 + 21*x1^10*x2^2*x3 + 34*x1^10*x2^2 + 11*x1^10*x2*x3^11 + 26*x1^10*x2*x3^10 + 78*x1^10*x2*x3^9 + 75*x1^10*x2*x3^8 + 67*x1^10*x2*x3^7 + 37*x1^10*x2*x3^6 + 75*x1^10*x2*x3^5 + 46*x1^10*x2*x3^4 + 73*x1^10*x2*x3^3 + 21*x1^10*x2*x3^2 + 47*x1^10*x2*x3 + 18*x1^10*x2 + 13*x1^10*x3^11 + 51*x1^10*x3^10 + 41*x1^10*x3^9 + 44*x1^10*x3^8 + 23*x1^10*x3^7 + 46*x1^10*x3^6 + 34*x1^10*x3^5 + 45*x1^10*x3^4 + 15*x1^10*x3^3 + 34*x1^10*x3^2 + 18*x1^10*x3 + 24*x1^10 + 11*x1^9*x2^11*x3^2 + 13*x1^9*x2^11*x3 + 27*x1^9*x2^11 + 11*x1^9*x2^10*x3^3 + 26*x1^9*x2^10*x3^2 + 78*x1^9*x2^10*x3 + 41*x1^9*x2^10 + 11*x1^9*x2^9*x3^4 + 26*x1^9*x2^9*x3^3 + 105*x1^9*x2^9*x3^2 + 82*x1^9*x2^9*x3 + 44*x1^9*x2^9 + 11*x1^9*x2^8*x3^5 + 26*x1^9*x2^8*x3^4 + 126*x1^9*x2^8*x3^3 + 116*x1^9*x2^8*x3^2 + 88*x1^9*x2^8*x3 + 30*x1^9*x2^8 + 11*x1^9*x2^7*x3^6 + 26*x1^9*x2^7*x3^5 + 126*x1^9*x2^7*x3^4 + 122*x1^9*x2^7*x3^3 + 111*x1^9*x2^7*x3^2 + 53*x1^9*x2^7*x3 + 47*x1^9*x2^7 + 11*x1^9*x2^6*x3^7 + 26*x1^9*x2^6*x3^6 + 126*x1^9*x2^6*x3^5 + 122*x1^9*x2^6*x3^4 + 122*x1^9*x2^6*x3^3 + 67*x1^9*x2^6*x3^2 + 93*x1^9*x2^6*x3 + 46*x1^9*x2^6 + 11*x1^9*x2^5*x3^8 + 26*x1^9*x2^5*x3^7 + 126*x1^9*x2^5*x3^6 + 122*x1^9*x2^5*x3^5 + 122*x1^9*x2^5*x3^4 + 73*x1^9*x2^5*x3^3 + 122*x1^9*x2^5*x3^2 + 80*x1^9*x2^5*x3 + 70*x1^9*x2^5 + 11*x1^9*x2^4*x3^9 + 26*x1^9*x2^4*x3^8 + 126*x1^9*x2^4*x3^7 + 122*x1^9*x2^4*x3^6 + 122*x1^9*x2^4*x3^5 + 73*x1^9*x2^4*x3^4 + 143*x1^9*x2^4*x3^3 + 92*x1^9*x2^4*x3^2 + 115*x1^9*x2^4*x3 + 40*x1^9*x2^4 + 11*x1^9*x2^3*x3^10 + 26*x1^9*x2^3*x3^9 + 126*x1^9*x2^3*x3^8 + 122*x1^9*x2^3*x3^7 + 122*x1^9*x2^3*x3^6 + 73*x1^9*x2^3*x3^5 + 143*x1^9*x2^3*x3^4 + 92*x1^9*x2^3*x3^3 + 143*x1^9*x2^3*x3^2 + 55*x1^9*x2^3*x3 + 46*x1^9*x2^3 + 11*x1^9*x2^2*x3^11 + 26*x1^9*x2^2*x3^10 + 105*x1^9*x2^2*x3^9 + 116*x1^9*x2^2*x3^8 + 111*x1^9*x2^2*x3^7 + 67*x1^9*x2^2*x3^6 + 122*x1^9*x2^2*x3^5 + 92*x1^9*x2^2*x3^4 + 143*x1^9*x2^2*x3^3 + 61*x1^9*x2^2*x3^2 + 80*x1^9*x2^2*x3 + 19*x1^9*x2^2 + 13*x1^9*x2*x3^11 + 78*x1^9*x2*x3^10 + 82*x1^9*x2*x3^9 + 88*x1^9*x2*x3^8 + 53*x1^9*x2*x3^7 + 93*x1^9*x2*x3^6 + 80*x1^9*x2*x3^5 + 115*x1^9*x2*x3^4 + 55*x1^9*x2*x3^3 + 80*x1^9*x2*x3^2 + 26*x1^9*x2*x3 + 31*x1^9*x2 + 27*x1^9*x3^11 + 41*x1^9*x3^10 + 44*x1^9*x3^9 + 30*x1^9*x3^8 + 47*x1^9*x3^7 + 46*x1^9*x3^6 + 70*x1^9*x3^5 + 40*x1^9*x3^4 + 46*x1^9*x3^3 + 19*x1^9*x3^2 + 31*x1^9*x3 + 21*x1^8*x2^12 + 11*x1^8*x2^11*x3^3 + 13*x1^8*x2^11*x3^2 + 48*x1^8*x2^11*x3 + 34*x1^8*x2^11 + 11*x1^8*x2^10*x3^4 + 26*x1^8*x2^10*x3^3 + 99*x1^8*x2^10*x3^2 + 75*x1^8*x2^10*x3 + 44*x1^8*x2^10 + 11*x1^8*x2^9*x3^5 + 26*x1^8*x2^9*x3^4 + 126*x1^8*x2^9*x3^3 + 116*x1^8*x2^9*x3^2 + 88*x1^8*x2^9*x3 + 30*x1^8*x2^9 + 11*x1^8*x2^8*x3^6 + 26*x1^8*x2^8*x3^5 + 147*x1^8*x2^8*x3^4 + 150*x1^8*x2^8*x3^3 + 132*x1^8*x2^8*x3^2 + 60*x1^8*x2^8*x3 + 72*x1^8*x2^8 + 11*x1^8*x2^7*x3^7 + 26*x1^8*x2^7*x3^6 + 147*x1^8*x2^7*x3^5 + 156*x1^8*x2^7*x3^4 + 155*x1^8*x2^7*x3^3 + 83*x1^8*x2^7*x3^2 + 119*x1^8*x2^7*x3 + 61*x1^8*x2^7 + 11*x1^8*x2^6*x3^8 + 26*x1^8*x2^6*x3^7 + 147*x1^8*x2^6*x3^6 + 156*x1^8*x2^6*x3^5 + 166*x1^8*x2^6*x3^4 + 97*x1^8*x2^6*x3^3 + 165*x1^8*x2^6*x3^2 + 107*x1^8*x2^6*x3 + 73*x1^8*x2^6 + 11*x1^8*x2^5*x3^9 + 26*x1^8*x2^5*x3^8 + 147*x1^8*x2^5*x3^7 + 156*x1^8*x2^5*x3^6 + 166*x1^8*x2^5*x3^5 + 103*x1^8*x2^5*x3^4 + 194*x1^8*x2^5*x3^3 + 141*x1^8*x2^5*x3^2 + 143*x1^8*x2^5*x3 + 58*x1^8*x2^5 + 11*x1^8*x2^4*x3^10 + 26*x1^8*x2^4*x3^9 + 147*x1^8*x2^4*x3^8 + 156*x1^8*x2^4*x3^7 + 166*x1^8*x2^4*x3^6 + 103*x1^8*x2^4*x3^5 + 215*x1^8*x2^4*x3^4 + 153*x1^8*x2^4*x3^3 + 188*x1^8*x2^4*x3^2 + 98*x1^8*x2^4*x3 + 83*x1^8*x2^4 + 11*x1^8*x2^3*x3^11 + 26*x1^8*x2^3*x3^10 + 126*x1^8*x2^3*x3^9 + 150*x1^8*x2^3*x3^8 + 155*x1^8*x2^3*x3^7 + 97*x1^8*x2^3*x3^6 + 194*x1^8*x2^3*x3^5 + 153*x1^8*x2^3*x3^4 + 216*x1^8*x2^3*x3^3 + 113*x1^8*x2^3*x3^2 + 129*x1^8*x2^3*x3 + 37*x1^8*x2^3 + 13*x1^8*x2^2*x3^11 + 99*x1^8*x2^2*x3^10 + 116*x1^8*x2^2*x3^9 + 132*x1^8*x2^2*x3^8 + 83*x1^8*x2^2*x3^7 + 165*x1^8*x2^2*x3^6 + 141*x1^8*x2^2*x3^5 + 188*x1^8*x2^2*x3^4 + 113*x1^8*x2^2*x3^3 + 150*x1^8*x2^2*x3^2 + 45*x1^8*x2^2*x3 + 34*x1^8*x2^2 + 48*x1^8*x2*x3^11 + 75*x1^8*x2*x3^10 + 88*x1^8*x2*x3^9 + 60*x1^8*x2*x3^8 + 119*x1^8*x2*x3^7 + 107*x1^8*x2*x3^6 + 143*x1^8*x2*x3^5 + 98*x1^8*x2*x3^4 + 129*x1^8*x2*x3^3 + 45*x1^8*x2*x3^2 + 41*x1^8*x2*x3 + 15*x1^8*x2 + 21*x1^8*x3^12 + 34*x1^8*x3^11 + 44*x1^8*x3^10 + 30*x1^8*x3^9 + 72*x1^8*x3^8 + 61*x1^8*x3^7 + 73*x1^8*x3^6 + 58*x1^8*x3^5 + 83*x1^8*x3^4 + 37*x1^8*x3^3 + 34*x1^8*x3^2 + 15*x1^8*x3 + 25*x1^8 + 21*x1^7*x2^12*x3 + 6*x1^7*x2^12 + 11*x1^7*x2^11*x3^4 + 13*x1^7*x2^11*x3^3 + 48*x1^7*x2^11*x3^2 + 40*x1^7*x2^11*x3 + 23*x1^7*x2^11 + 11*x1^7*x2^10*x3^5 + 26*x1^7*x2^10*x3^4 + 99*x1^7*x2^10*x3^3 + 81*x1^7*x2^10*x3^2 + 67*x1^7*x2^10*x3 + 23*x1^7*x2^10 + 11*x1^7*x2^9*x3^6 + 26*x1^7*x2^9*x3^5 + 126*x1^7*x2^9*x3^4 + 122*x1^7*x2^9*x3^3 + 111*x1^7*x2^9*x3^2 + 53*x1^7*x2^9*x3 + 47*x1^7*x2^9 + 11*x1^7*x2^8*x3^7 + 26*x1^7*x2^8*x3^6 + 147*x1^7*x2^8*x3^5 + 156*x1^7*x2^8*x3^4 + 155*x1^7*x2^8*x3^3 + 83*x1^7*x2^8*x3^2 + 119*x1^7*x2^8*x3 + 61*x1^7*x2^8 + 11*x1^7*x2^7*x3^8 + 26*x1^7*x2^7*x3^7 + 147*x1^7*x2^7*x3^6 + 162*x1^7*x2^7*x3^5 + 178*x1^7*x2^7*x3^4 + 106*x1^7*x2^7*x3^3 + 166*x1^7*x2^7*x3^2 + 122*x1^7*x2^7*x3 + 103*x1^7*x2^7 + 11*x1^7*x2^6*x3^9 + 26*x1^7*x2^6*x3^8 + 147*x1^7*x2^6*x3^7 + 162*x1^7*x2^6*x3^6 + 189*x1^7*x2^6*x3^5 + 120*x1^7*x2^6*x3^4 + 212*x1^7*x2^6*x3^3 + 168*x1^7*x2^6*x3^2 + 176*x1^7*x2^6*x3 + 60*x1^7*x2^6 + 11*x1^7*x2^5*x3^10 + 26*x1^7*x2^5*x3^9 + 147*x1^7*x2^5*x3^8 + 162*x1^7*x2^5*x3^7 + 189*x1^7*x2^5*x3^6 + 126*x1^7*x2^5*x3^5 + 241*x1^7*x2^5*x3^4 + 202*x1^7*x2^5*x3^3 + 246*x1^7*x2^5*x3^2 + 118*x1^7*x2^5*x3 + 93*x1^7*x2^5 + 11*x1^7*x2^4*x3^11 + 26*x1^7*x2^4*x3^10 + 126*x1^7*x2^4*x3^9 + 156*x1^7*x2^4*x3^8 + 178*x1^7*x2^4*x3^7 + 120*x1^7*x2^4*x3^6 + 241*x1^7*x2^4*x3^5 + 214*x1^7*x2^4*x3^4 + 291*x1^7*x2^4*x3^3 + 158*x1^7*x2^4*x3^2 + 176*x1^7*x2^4*x3 + 64*x1^7*x2^4 + 13*x1^7*x2^3*x3^11 + 99*x1^7*x2^3*x3^10 + 122*x1^7*x2^3*x3^9 + 155*x1^7*x2^3*x3^8 + 106*x1^7*x2^3*x3^7 + 212*x1^7*x2^3*x3^6 + 202*x1^7*x2^3*x3^5 + 291*x1^7*x2^3*x3^4 + 167*x1^7*x2^3*x3^3 + 209*x1^7*x2^3*x3^2 + 90*x1^7*x2^3*x3 + 61*x1^7*x2^3 + 48*x1^7*x2^2*x3^11 + 81*x1^7*x2^2*x3^10 + 111*x1^7*x2^2*x3^9 + 83*x1^7*x2^2*x3^8 + 166*x1^7*x2^2*x3^7 + 168*x1^7*x2^2*x3^6 + 246*x1^7*x2^2*x3^5 + 158*x1^7*x2^2*x3^4 + 209*x1^7*x2^2*x3^3 + 91*x1^7*x2^2*x3^2 + 71*x1^7*x2^2*x3 + 25*x1^7*x2^2 + 21*x1^7*x2*x3^12 + 40*x1^7*x2*x3^11 + 67*x1^7*x2*x3^10 + 53*x1^7*x2*x3^9 + 119*x1^7*x2*x3^8 + 122*x1^7*x2*x3^7 + 176*x1^7*x2*x3^6 + 118*x1^7*x2*x3^5 + 176*x1^7*x2*x3^4 + 90*x1^7*x2*x3^3 + 71*x1^7*x2*x3^2 + 40*x1^7*x2*x3 + 27*x1^7*x2 + 6*x1^7*x3^12 + 23*x1^7*x3^11 + 23*x1^7*x3^10 + 47*x1^7*x3^9 + 61*x1^7*x3^8 + 103*x1^7*x3^7 + 60*x1^7*x3^6 + 93*x1^7*x3^5 + 64*x1^7*x3^4 + 61*x1^7*x3^3 + 25*x1^7*x3^2 + 27*x1^7*x3 + 30*x1^7 + 21*x1^6*x2^12*x3^2 + 6*x1^6*x2^12*x3 + 11*x1^6*x2^12 + 11*x1^6*x2^11*x3^5 + 13*x1^6*x2^11*x3^4 + 48*x1^6*x2^11*x3^3 + 40*x1^6*x2^11*x3^2 + 34*x1^6*x2^11*x3 + 14*x1^6*x2^11 + 11*x1^6*x2^10*x3^6 + 26*x1^6*x2^10*x3^5 + 99*x1^6*x2^10*x3^4 + 81*x1^6*x2^10*x3^3 + 78*x1^6*x2^10*x3^2 + 37*x1^6*x2^10*x3 + 46*x1^6*x2^10 + 11*x1^6*x2^9*x3^7 + 26*x1^6*x2^9*x3^6 + 126*x1^6*x2^9*x3^5 + 122*x1^6*x2^9*x3^4 + 122*x1^6*x2^9*x3^3 + 67*x1^6*x2^9*x3^2 + 93*x1^6*x2^9*x3 + 46*x1^6*x2^9 + 11*x1^6*x2^8*x3^8 + 26*x1^6*x2^8*x3^7 + 147*x1^6*x2^8*x3^6 + 156*x1^6*x2^8*x3^5 + 166*x1^6*x2^8*x3^4 + 97*x1^6*x2^8*x3^3 + 165*x1^6*x2^8*x3^2 + 107*x1^6*x2^8*x3 + 73*x1^6*x2^8 + 11*x1^6*x2^7*x3^9 + 26*x1^6*x2^7*x3^8 + 147*x1^6*x2^7*x3^7 + 162*x1^6*x2^7*x3^6 + 189*x1^6*x2^7*x3^5 + 120*x1^6*x2^7*x3^4 + 212*x1^6*x2^7*x3^3 + 168*x1^6*x2^7*x3^2 + 176*x1^6*x2^7*x3 + 60*x1^6*x2^7 + 11*x1^6*x2^6*x3^10 + 26*x1^6*x2^6*x3^9 + 147*x1^6*x2^6*x3^8 + 162*x1^6*x2^6*x3^7 + 200*x1^6*x2^6*x3^6 + 134*x1^6*x2^6*x3^5 + 258*x1^6*x2^6*x3^4 + 214*x1^6*x2^6*x3^3 + 249*x1^6*x2^6*x3^2 + 120*x1^6*x2^6*x3 + 101*x1^6*x2^6 + 11*x1^6*x2^5*x3^11 + 26*x1^6*x2^5*x3^10 + 126*x1^6*x2^5*x3^9 + 156*x1^6*x2^5*x3^8 + 189*x1^6*x2^5*x3^7 + 134*x1^6*x2^5*x3^6 + 266*x1^6*x2^5*x3^5 + 248*x1^6*x2^5*x3^4 + 319*x1^6*x2^5*x3^3 + 178*x1^6*x2^5*x3^2 + 194*x1^6*x2^5*x3 + 73*x1^6*x2^5 + 13*x1^6*x2^4*x3^11 + 99*x1^6*x2^4*x3^10 + 122*x1^6*x2^4*x3^9 + 166*x1^6*x2^4*x3^8 + 120*x1^6*x2^4*x3^7 + 258*x1^6*x2^4*x3^6 + 248*x1^6*x2^4*x3^5 + 336*x1^6*x2^4*x3^4 + 212*x1^6*x2^4*x3^3 + 264*x1^6*x2^4*x3^2 + 126*x1^6*x2^4*x3 + 103*x1^6*x2^4 + 48*x1^6*x2^3*x3^11 + 81*x1^6*x2^3*x3^10 + 122*x1^6*x2^3*x3^9 + 97*x1^6*x2^3*x3^8 + 212*x1^6*x2^3*x3^7 + 214*x1^6*x2^3*x3^6 + 319*x1^6*x2^3*x3^5 + 212*x1^6*x2^3*x3^4 + 276*x1^6*x2^3*x3^3 + 145*x1^6*x2^3*x3^2 + 140*x1^6*x2^3*x3 + 57*x1^6*x2^3 + 21*x1^6*x2^2*x3^12 + 40*x1^6*x2^2*x3^11 + 78*x1^6*x2^2*x3^10 + 67*x1^6*x2^2*x3^9 + 165*x1^6*x2^2*x3^8 + 168*x1^6*x2^2*x3^7 + 249*x1^6*x2^2*x3^6 + 178*x1^6*x2^2*x3^5 + 264*x1^6*x2^2*x3^4 + 145*x1^6*x2^2*x3^3 + 143*x1^6*x2^2*x3^2 + 82*x1^6*x2^2*x3 + 69*x1^6*x2^2 + 6*x1^6*x2*x3^12 + 34*x1^6*x2*x3^11 + 37*x1^6*x2*x3^10 + 93*x1^6*x2*x3^9 + 107*x1^6*x2*x3^8 + 176*x1^6*x2*x3^7 + 120*x1^6*x2*x3^6 + 194*x1^6*x2*x3^5 + 126*x1^6*x2*x3^4 + 140*x1^6*x2*x3^3 + 82*x1^6*x2*x3^2 + 71*x1^6*x2*x3 + 39*x1^6*x2 + 11*x1^6*x3^12 + 14*x1^6*x3^11 + 46*x1^6*x3^10 + 46*x1^6*x3^9 + 73*x1^6*x3^8 + 60*x1^6*x3^7 + 101*x1^6*x3^6 + 73*x1^6*x3^5 + 103*x1^6*x3^4 + 57*x1^6*x3^3 + 69*x1^6*x3^2 + 39*x1^6*x3 + 8*x1^6 + 21*x1^5*x2^12*x3^3 + 6*x1^5*x2^12*x3^2 + 11*x1^5*x2^12*x3 + 6*x1^5*x2^12 + 11*x1^5*x2^11*x3^6 + 13*x1^5*x2^11*x3^5 + 48*x1^5*x2^11*x3^4 + 40*x1^5*x2^11*x3^3 + 34*x1^5*x2^11*x3^2 + 20*x1^5*x2^11*x3 + 29*x1^5*x2^11 + 11*x1^5*x2^10*x3^7 + 26*x1^5*x2^10*x3^6 + 99*x1^5*x2^10*x3^5 + 81*x1^5*x2^10*x3^4 + 78*x1^5*x2^10*x3^3 + 43*x1^5*x2^10*x3^2 + 75*x1^5*x2^10*x3 + 34*x1^5*x2^10 + 11*x1^5*x2^9*x3^8 + 26*x1^5*x2^9*x3^7 + 126*x1^5*x2^9*x3^6 + 122*x1^5*x2^9*x3^5 + 122*x1^5*x2^9*x3^4 + 73*x1^5*x2^9*x3^3 + 122*x1^5*x2^9*x3^2 + 80*x1^5*x2^9*x3 + 70*x1^5*x2^9 + 11*x1^5*x2^8*x3^9 + 26*x1^5*x2^8*x3^8 + 147*x1^5*x2^8*x3^7 + 156*x1^5*x2^8*x3^6 + 166*x1^5*x2^8*x3^5 + 103*x1^5*x2^8*x3^4 + 194*x1^5*x2^8*x3^3 + 141*x1^5*x2^8*x3^2 + 143*x1^5*x2^8*x3 + 58*x1^5*x2^8 + 11*x1^5*x2^7*x3^10 + 26*x1^5*x2^7*x3^9 + 147*x1^5*x2^7*x3^8 + 162*x1^5*x2^7*x3^7 + 189*x1^5*x2^7*x3^6 + 126*x1^5*x2^7*x3^5 + 241*x1^5*x2^7*x3^4 + 202*x1^5*x2^7*x3^3 + 246*x1^5*x2^7*x3^2 + 118*x1^5*x2^7*x3 + 93*x1^5*x2^7 + 11*x1^5*x2^6*x3^11 + 26*x1^5*x2^6*x3^10 + 126*x1^5*x2^6*x3^9 + 156*x1^5*x2^6*x3^8 + 189*x1^5*x2^6*x3^7 + 134*x1^5*x2^6*x3^6 + 266*x1^5*x2^6*x3^5 + 248*x1^5*x2^6*x3^4 + 319*x1^5*x2^6*x3^3 + 178*x1^5*x2^6*x3^2 + 194*x1^5*x2^6*x3 + 73*x1^5*x2^6 + 13*x1^5*x2^5*x3^11 + 99*x1^5*x2^5*x3^10 + 122*x1^5*x2^5*x3^9 + 166*x1^5*x2^5*x3^8 + 126*x1^5*x2^5*x3^7 + 266*x1^5*x2^5*x3^6 + 270*x1^5*x2^5*x3^5 + 361*x1^5*x2^5*x3^4 + 230*x1^5*x2^5*x3^3 + 274*x1^5*x2^5*x3^2 + 135*x1^5*x2^5*x3 + 103*x1^5*x2^5 + 48*x1^5*x2^4*x3^11 + 81*x1^5*x2^4*x3^10 + 122*x1^5*x2^4*x3^9 + 103*x1^5*x2^4*x3^8 + 241*x1^5*x2^4*x3^7 + 248*x1^5*x2^4*x3^6 + 361*x1^5*x2^4*x3^5 + 255*x1^5*x2^4*x3^4 + 323*x1^5*x2^4*x3^3 + 181*x1^5*x2^4*x3^2 + 182*x1^5*x2^4*x3 + 72*x1^5*x2^4 + 21*x1^5*x2^3*x3^12 + 40*x1^5*x2^3*x3^11 + 78*x1^5*x2^3*x3^10 + 73*x1^5*x2^3*x3^9 + 194*x1^5*x2^3*x3^8 + 202*x1^5*x2^3*x3^7 + 319*x1^5*x2^3*x3^6 + 230*x1^5*x2^3*x3^5 + 323*x1^5*x2^3*x3^4 + 199*x1^5*x2^3*x3^3 + 212*x1^5*x2^3*x3^2 + 129*x1^5*x2^3*x3 + 76*x1^5*x2^3 + 6*x1^5*x2^2*x3^12 + 34*x1^5*x2^2*x3^11 + 43*x1^5*x2^2*x3^10 + 122*x1^5*x2^2*x3^9 + 141*x1^5*x2^2*x3^8 + 246*x1^5*x2^2*x3^7 + 178*x1^5*x2^2*x3^6 + 274*x1^5*x2^2*x3^5 + 181*x1^5*x2^2*x3^4 + 212*x1^5*x2^2*x3^3 + 139*x1^5*x2^2*x3^2 + 120*x1^5*x2^2*x3 + 46*x1^5*x2^2 + 11*x1^5*x2*x3^12 + 20*x1^5*x2*x3^11 + 75*x1^5*x2*x3^10 + 80*x1^5*x2*x3^9 + 143*x1^5*x2*x3^8 + 118*x1^5*x2*x3^7 + 194*x1^5*x2*x3^6 + 135*x1^5*x2*x3^5 + 182*x1^5*x2*x3^4 + 129*x1^5*x2*x3^3 + 120*x1^5*x2*x3^2 + 55*x1^5*x2*x3 + 23*x1^5*x2 + 6*x1^5*x3^12 + 29*x1^5*x3^11 + 34*x1^5*x3^10 + 70*x1^5*x3^9 + 58*x1^5*x3^8 + 93*x1^5*x3^7 + 73*x1^5*x3^6 + 103*x1^5*x3^5 + 72*x1^5*x3^4 + 76*x1^5*x3^3 + 46*x1^5*x3^2 + 23*x1^5*x3 + 21*x1^4*x2^12*x3^4 + 6*x1^4*x2^12*x3^3 + 11*x1^4*x2^12*x3^2 + 6*x1^4*x2^12*x3 + 21*x1^4*x2^12 + 11*x1^4*x2^11*x3^7 + 13*x1^4*x2^11*x3^6 + 48*x1^4*x2^11*x3^5 + 40*x1^4*x2^11*x3^4 + 34*x1^4*x2^11*x3^3 + 20*x1^4*x2^11*x3^2 + 50*x1^4*x2^11*x3 + 12*x1^4*x2^11 + 11*x1^4*x2^10*x3^8 + 26*x1^4*x2^10*x3^7 + 99*x1^4*x2^10*x3^6 + 81*x1^4*x2^10*x3^5 + 78*x1^4*x2^10*x3^4 + 43*x1^4*x2^10*x3^3 + 96*x1^4*x2^10*x3^2 + 46*x1^4*x2^10*x3 + 45*x1^4*x2^10 + 11*x1^4*x2^9*x3^9 + 26*x1^4*x2^9*x3^8 + 126*x1^4*x2^9*x3^7 + 122*x1^4*x2^9*x3^6 + 122*x1^4*x2^9*x3^5 + 73*x1^4*x2^9*x3^4 + 143*x1^4*x2^9*x3^3 + 92*x1^4*x2^9*x3^2 + 115*x1^4*x2^9*x3 + 40*x1^4*x2^9 + 11*x1^4*x2^8*x3^10 + 26*x1^4*x2^8*x3^9 + 147*x1^4*x2^8*x3^8 + 156*x1^4*x2^8*x3^7 + 166*x1^4*x2^8*x3^6 + 103*x1^4*x2^8*x3^5 + 215*x1^4*x2^8*x3^4 + 153*x1^4*x2^8*x3^3 + 188*x1^4*x2^8*x3^2 + 98*x1^4*x2^8*x3 + 83*x1^4*x2^8 + 11*x1^4*x2^7*x3^11 + 26*x1^4*x2^7*x3^10 + 126*x1^4*x2^7*x3^9 + 156*x1^4*x2^7*x3^8 + 178*x1^4*x2^7*x3^7 + 120*x1^4*x2^7*x3^6 + 241*x1^4*x2^7*x3^5 + 214*x1^4*x2^7*x3^4 + 291*x1^4*x2^7*x3^3 + 158*x1^4*x2^7*x3^2 + 176*x1^4*x2^7*x3 + 64*x1^4*x2^7 + 13*x1^4*x2^6*x3^11 + 99*x1^4*x2^6*x3^10 + 122*x1^4*x2^6*x3^9 + 166*x1^4*x2^6*x3^8 + 120*x1^4*x2^6*x3^7 + 258*x1^4*x2^6*x3^6 + 248*x1^4*x2^6*x3^5 + 336*x1^4*x2^6*x3^4 + 212*x1^4*x2^6*x3^3 + 264*x1^4*x2^6*x3^2 + 126*x1^4*x2^6*x3 + 103*x1^4*x2^6 + 48*x1^4*x2^5*x3^11 + 81*x1^4*x2^5*x3^10 + 122*x1^4*x2^5*x3^9 + 103*x1^4*x2^5*x3^8 + 241*x1^4*x2^5*x3^7 + 248*x1^4*x2^5*x3^6 + 361*x1^4*x2^5*x3^5 + 255*x1^4*x2^5*x3^4 + 323*x1^4*x2^5*x3^3 + 181*x1^4*x2^5*x3^2 + 182*x1^4*x2^5*x3 + 72*x1^4*x2^5 + 21*x1^4*x2^4*x3^12 + 40*x1^4*x2^4*x3^11 + 78*x1^4*x2^4*x3^10 + 73*x1^4*x2^4*x3^9 + 215*x1^4*x2^4*x3^8 + 214*x1^4*x2^4*x3^7 + 336*x1^4*x2^4*x3^6 + 255*x1^4*x2^4*x3^5 + 360*x1^4*x2^4*x3^4 + 226*x1^4*x2^4*x3^3 + 254*x1^4*x2^4*x3^2 + 144*x1^4*x2^4*x3 + 99*x1^4*x2^4 + 6*x1^4*x2^3*x3^12 + 34*x1^4*x2^3*x3^11 + 43*x1^4*x2^3*x3^10 + 143*x1^4*x2^3*x3^9 + 153*x1^4*x2^3*x3^8 + 291*x1^4*x2^3*x3^7 + 212*x1^4*x2^3*x3^6 + 323*x1^4*x2^3*x3^5 + 226*x1^4*x2^3*x3^4 + 281*x1^4*x2^3*x3^3 + 186*x1^4*x2^3*x3^2 + 150*x1^4*x2^3*x3 + 60*x1^4*x2^3 + 11*x1^4*x2^2*x3^12 + 20*x1^4*x2^2*x3^11 + 96*x1^4*x2^2*x3^10 + 92*x1^4*x2^2*x3^9 + 188*x1^4*x2^2*x3^8 + 158*x1^4*x2^2*x3^7 + 264*x1^4*x2^2*x3^6 + 181*x1^4*x2^2*x3^5 + 254*x1^4*x2^2*x3^4 + 186*x1^4*x2^2*x3^3 + 192*x1^4*x2^2*x3^2 + 76*x1^4*x2^2*x3 + 31*x1^4*x2^2 + 6*x1^4*x2*x3^12 + 50*x1^4*x2*x3^11 + 46*x1^4*x2*x3^10 + 115*x1^4*x2*x3^9 + 98*x1^4*x2*x3^8 + 176*x1^4*x2*x3^7 + 126*x1^4*x2*x3^6 + 182*x1^4*x2*x3^5 + 144*x1^4*x2*x3^4 + 150*x1^4*x2*x3^3 + 76*x1^4*x2*x3^2 + 46*x1^4*x2*x3 + 14*x1^4*x2 + 21*x1^4*x3^12 + 12*x1^4*x3^11 + 45*x1^4*x3^10 + 40*x1^4*x3^9 + 83*x1^4*x3^8 + 64*x1^4*x3^7 + 103*x1^4*x3^6 + 72*x1^4*x3^5 + 99*x1^4*x3^4 + 60*x1^4*x3^3 + 31*x1^4*x3^2 + 14*x1^4*x3 + 23*x1^4 + 21*x1^3*x2^12*x3^5 + 6*x1^3*x2^12*x3^4 + 11*x1^3*x2^12*x3^3 + 6*x1^3*x2^12*x3^2 + 21*x1^3*x2^12*x3 + 11*x1^3*x2^11*x3^8 + 13*x1^3*x2^11*x3^7 + 48*x1^3*x2^11*x3^6 + 40*x1^3*x2^11*x3^5 + 34*x1^3*x2^11*x3^4 + 20*x1^3*x2^11*x3^3 + 50*x1^3*x2^11*x3^2 + 12*x1^3*x2^11*x3 + 28*x1^3*x2^11 + 11*x1^3*x2^10*x3^9 + 26*x1^3*x2^10*x3^8 + 99*x1^3*x2^10*x3^7 + 81*x1^3*x2^10*x3^6 + 78*x1^3*x2^10*x3^5 + 43*x1^3*x2^10*x3^4 + 96*x1^3*x2^10*x3^3 + 46*x1^3*x2^10*x3^2 + 73*x1^3*x2^10*x3 + 15*x1^3*x2^10 + 11*x1^3*x2^9*x3^10 + 26*x1^3*x2^9*x3^9 + 126*x1^3*x2^9*x3^8 + 122*x1^3*x2^9*x3^7 + 122*x1^3*x2^9*x3^6 + 73*x1^3*x2^9*x3^5 + 143*x1^3*x2^9*x3^4 + 92*x1^3*x2^9*x3^3 + 143*x1^3*x2^9*x3^2 + 55*x1^3*x2^9*x3 + 46*x1^3*x2^9 + 11*x1^3*x2^8*x3^11 + 26*x1^3*x2^8*x3^10 + 126*x1^3*x2^8*x3^9 + 150*x1^3*x2^8*x3^8 + 155*x1^3*x2^8*x3^7 + 97*x1^3*x2^8*x3^6 + 194*x1^3*x2^8*x3^5 + 153*x1^3*x2^8*x3^4 + 216*x1^3*x2^8*x3^3 + 113*x1^3*x2^8*x3^2 + 129*x1^3*x2^8*x3 + 37*x1^3*x2^8 + 13*x1^3*x2^7*x3^11 + 99*x1^3*x2^7*x3^10 + 122*x1^3*x2^7*x3^9 + 155*x1^3*x2^7*x3^8 + 106*x1^3*x2^7*x3^7 + 212*x1^3*x2^7*x3^6 + 202*x1^3*x2^7*x3^5 + 291*x1^3*x2^7*x3^4 + 167*x1^3*x2^7*x3^3 + 209*x1^3*x2^7*x3^2 + 90*x1^3*x2^7*x3 + 61*x1^3*x2^7 + 48*x1^3*x2^6*x3^11 + 81*x1^3*x2^6*x3^10 + 122*x1^3*x2^6*x3^9 + 97*x1^3*x2^6*x3^8 + 212*x1^3*x2^6*x3^7 + 214*x1^3*x2^6*x3^6 + 319*x1^3*x2^6*x3^5 + 212*x1^3*x2^6*x3^4 + 276*x1^3*x2^6*x3^3 + 145*x1^3*x2^6*x3^2 + 140*x1^3*x2^6*x3 + 57*x1^3*x2^6 + 21*x1^3*x2^5*x3^12 + 40*x1^3*x2^5*x3^11 + 78*x1^3*x2^5*x3^10 + 73*x1^3*x2^5*x3^9 + 194*x1^3*x2^5*x3^8 + 202*x1^3*x2^5*x3^7 + 319*x1^3*x2^5*x3^6 + 230*x1^3*x2^5*x3^5 + 323*x1^3*x2^5*x3^4 + 199*x1^3*x2^5*x3^3 + 212*x1^3*x2^5*x3^2 + 129*x1^3*x2^5*x3 + 76*x1^3*x2^5 + 6*x1^3*x2^4*x3^12 + 34*x1^3*x2^4*x3^11 + 43*x1^3*x2^4*x3^10 + 143*x1^3*x2^4*x3^9 + 153*x1^3*x2^4*x3^8 + 291*x1^3*x2^4*x3^7 + 212*x1^3*x2^4*x3^6 + 323*x1^3*x2^4*x3^5 + 226*x1^3*x2^4*x3^4 + 281*x1^3*x2^4*x3^3 + 186*x1^3*x2^4*x3^2 + 150*x1^3*x2^4*x3 + 60*x1^3*x2^4 + 11*x1^3*x2^3*x3^12 + 20*x1^3*x2^3*x3^11 + 96*x1^3*x2^3*x3^10 + 92*x1^3*x2^3*x3^9 + 216*x1^3*x2^3*x3^8 + 167*x1^3*x2^3*x3^7 + 276*x1^3*x2^3*x3^6 + 199*x1^3*x2^3*x3^5 + 281*x1^3*x2^3*x3^4 + 218*x1^3*x2^3*x3^3 + 199*x1^3*x2^3*x3^2 + 90*x1^3*x2^3*x3 + 32*x1^3*x2^3 + 6*x1^3*x2^2*x3^12 + 50*x1^3*x2^2*x3^11 + 46*x1^3*x2^2*x3^10 + 143*x1^3*x2^2*x3^9 + 113*x1^3*x2^2*x3^8 + 209*x1^3*x2^2*x3^7 + 145*x1^3*x2^2*x3^6 + 212*x1^3*x2^2*x3^5 + 186*x1^3*x2^2*x3^4 + 199*x1^3*x2^2*x3^3 + 97*x1^3*x2^2*x3^2 + 55*x1^3*x2^2*x3 + 25*x1^3*x2^2 + 21*x1^3*x2*x3^12 + 12*x1^3*x2*x3^11 + 73*x1^3*x2*x3^10 + 55*x1^3*x2*x3^9 + 129*x1^3*x2*x3^8 + 90*x1^3*x2*x3^7 + 140*x1^3*x2*x3^6 + 129*x1^3*x2*x3^5 + 150*x1^3*x2*x3^4 + 90*x1^3*x2*x3^3 + 55*x1^3*x2*x3^2 + 39*x1^3*x2*x3 + 34*x1^3*x2 + 28*x1^3*x3^11 + 15*x1^3*x3^10 + 46*x1^3*x3^9 + 37*x1^3*x3^8 + 61*x1^3*x3^7 + 57*x1^3*x3^6 + 76*x1^3*x3^5 + 60*x1^3*x3^4 + 32*x1^3*x3^3 + 25*x1^3*x3^2 + 34*x1^3*x3 + x1^3 + 21*x1^2*x2^12*x3^6 + 6*x1^2*x2^12*x3^5 + 11*x1^2*x2^12*x3^4 + 6*x1^2*x2^12*x3^3 + 21*x1^2*x2^12*x3^2 + 11*x1^2*x2^11*x3^9 + 13*x1^2*x2^11*x3^8 + 48*x1^2*x2^11*x3^7 + 40*x1^2*x2^11*x3^6 + 34*x1^2*x2^11*x3^5 + 20*x1^2*x2^11*x3^4 + 50*x1^2*x2^11*x3^3 + 12*x1^2*x2^11*x3^2 + 28*x1^2*x2^11*x3 + 6*x1^2*x2^11 + 11*x1^2*x2^10*x3^10 + 26*x1^2*x2^10*x3^9 + 99*x1^2*x2^10*x3^8 + 81*x1^2*x2^10*x3^7 + 78*x1^2*x2^10*x3^6 + 43*x1^2*x2^10*x3^5 + 96*x1^2*x2^10*x3^4 + 46*x1^2*x2^10*x3^3 + 73*x1^2*x2^10*x3^2 + 21*x1^2*x2^10*x3 + 34*x1^2*x2^10 + 11*x1^2*x2^9*x3^11 + 26*x1^2*x2^9*x3^10 + 105*x1^2*x2^9*x3^9 + 116*x1^2*x2^9*x3^8 + 111*x1^2*x2^9*x3^7 + 67*x1^2*x2^9*x3^6 + 122*x1^2*x2^9*x3^5 + 92*x1^2*x2^9*x3^4 + 143*x1^2*x2^9*x3^3 + 61*x1^2*x2^9*x3^2 + 80*x1^2*x2^9*x3 + 19*x1^2*x2^9 + 13*x1^2*x2^8*x3^11 + 99*x1^2*x2^8*x3^10 + 116*x1^2*x2^8*x3^9 + 132*x1^2*x2^8*x3^8 + 83*x1^2*x2^8*x3^7 + 165*x1^2*x2^8*x3^6 + 141*x1^2*x2^8*x3^5 + 188*x1^2*x2^8*x3^4 + 113*x1^2*x2^8*x3^3 + 150*x1^2*x2^8*x3^2 + 45*x1^2*x2^8*x3 + 34*x1^2*x2^8 + 48*x1^2*x2^7*x3^11 + 81*x1^2*x2^7*x3^10 + 111*x1^2*x2^7*x3^9 + 83*x1^2*x2^7*x3^8 + 166*x1^2*x2^7*x3^7 + 168*x1^2*x2^7*x3^6 + 246*x1^2*x2^7*x3^5 + 158*x1^2*x2^7*x3^4 + 209*x1^2*x2^7*x3^3 + 91*x1^2*x2^7*x3^2 + 71*x1^2*x2^7*x3 + 25*x1^2*x2^7 + 21*x1^2*x2^6*x3^12 + 40*x1^2*x2^6*x3^11 + 78*x1^2*x2^6*x3^10 + 67*x1^2*x2^6*x3^9 + 165*x1^2*x2^6*x3^8 + 168*x1^2*x2^6*x3^7 + 249*x1^2*x2^6*x3^6 + 178*x1^2*x2^6*x3^5 + 264*x1^2*x2^6*x3^4 + 145*x1^2*x2^6*x3^3 + 143*x1^2*x2^6*x3^2 + 82*x1^2*x2^6*x3 + 69*x1^2*x2^6 + 6*x1^2*x2^5*x3^12 + 34*x1^2*x2^5*x3^11 + 43*x1^2*x2^5*x3^10 + 122*x1^2*x2^5*x3^9 + 141*x1^2*x2^5*x3^8 + 246*x1^2*x2^5*x3^7 + 178*x1^2*x2^5*x3^6 + 274*x1^2*x2^5*x3^5 + 181*x1^2*x2^5*x3^4 + 212*x1^2*x2^5*x3^3 + 139*x1^2*x2^5*x3^2 + 120*x1^2*x2^5*x3 + 46*x1^2*x2^5 + 11*x1^2*x2^4*x3^12 + 20*x1^2*x2^4*x3^11 + 96*x1^2*x2^4*x3^10 + 92*x1^2*x2^4*x3^9 + 188*x1^2*x2^4*x3^8 + 158*x1^2*x2^4*x3^7 + 264*x1^2*x2^4*x3^6 + 181*x1^2*x2^4*x3^5 + 254*x1^2*x2^4*x3^4 + 186*x1^2*x2^4*x3^3 + 192*x1^2*x2^4*x3^2 + 76*x1^2*x2^4*x3 + 31*x1^2*x2^4 + 6*x1^2*x2^3*x3^12 + 50*x1^2*x2^3*x3^11 + 46*x1^2*x2^3*x3^10 + 143*x1^2*x2^3*x3^9 + 113*x1^2*x2^3*x3^8 + 209*x1^2*x2^3*x3^7 + 145*x1^2*x2^3*x3^6 + 212*x1^2*x2^3*x3^5 + 186*x1^2*x2^3*x3^4 + 199*x1^2*x2^3*x3^3 + 97*x1^2*x2^3*x3^2 + 55*x1^2*x2^3*x3 + 25*x1^2*x2^3 + 21*x1^2*x2^2*x3^12 + 12*x1^2*x2^2*x3^11 + 73*x1^2*x2^2*x3^10 + 61*x1^2*x2^2*x3^9 + 150*x1^2*x2^2*x3^8 + 91*x1^2*x2^2*x3^7 + 143*x1^2*x2^2*x3^6 + 139*x1^2*x2^2*x3^5 + 192*x1^2*x2^2*x3^4 + 97*x1^2*x2^2*x3^3 + 63*x1^2*x2^2*x3^2 + 50*x1^2*x2^2*x3 + 40*x1^2*x2^2 + 28*x1^2*x2*x3^11 + 21*x1^2*x2*x3^10 + 80*x1^2*x2*x3^9 + 45*x1^2*x2*x3^8 + 71*x1^2*x2*x3^7 + 82*x1^2*x2*x3^6 + 120*x1^2*x2*x3^5 + 76*x1^2*x2*x3^4 + 55*x1^2*x2*x3^3 + 50*x1^2*x2*x3^2 + 51*x1^2*x2*x3 + 33*x1^2*x2 + 6*x1^2*x3^11 + 34*x1^2*x3^10 + 19*x1^2*x3^9 + 34*x1^2*x3^8 + 25*x1^2*x3^7 + 69*x1^2*x3^6 + 46*x1^2*x3^5 + 31*x1^2*x3^4 + 25*x1^2*x3^3 + 40*x1^2*x3^2 + 33*x1^2*x3 + 6*x1^2 + 21*x1*x2^12*x3^7 + 6*x1*x2^12*x3^6 + 11*x1*x2^12*x3^5 + 6*x1*x2^12*x3^4 + 21*x1*x2^12*x3^3 + 11*x1*x2^11*x3^10 + 13*x1*x2^11*x3^9 + 48*x1*x2^11*x3^8 + 40*x1*x2^11*x3^7 + 34*x1*x2^11*x3^6 + 20*x1*x2^11*x3^5 + 50*x1*x2^11*x3^4 + 12*x1*x2^11*x3^3 + 28*x1*x2^11*x3^2 + 6*x1*x2^11*x3 + 13*x1*x2^11 + 11*x1*x2^10*x3^11 + 26*x1*x2^10*x3^10 + 78*x1*x2^10*x3^9 + 75*x1*x2^10*x3^8 + 67*x1*x2^10*x3^7 + 37*x1*x2^10*x3^6 + 75*x1*x2^10*x3^5 + 46*x1*x2^10*x3^4 + 73*x1*x2^10*x3^3 + 21*x1*x2^10*x3^2 + 47*x1*x2^10*x3 + 18*x1*x2^10 + 13*x1*x2^9*x3^11 + 78*x1*x2^9*x3^10 + 82*x1*x2^9*x3^9 + 88*x1*x2^9*x3^8 + 53*x1*x2^9*x3^7 + 93*x1*x2^9*x3^6 + 80*x1*x2^9*x3^5 + 115*x1*x2^9*x3^4 + 55*x1*x2^9*x3^3 + 80*x1*x2^9*x3^2 + 26*x1*x2^9*x3 + 31*x1*x2^9 + 48*x1*x2^8*x3^11 + 75*x1*x2^8*x3^10 + 88*x1*x2^8*x3^9 + 60*x1*x2^8*x3^8 + 119*x1*x2^8*x3^7 + 107*x1*x2^8*x3^6 + 143*x1*x2^8*x3^5 + 98*x1*x2^8*x3^4 + 129*x1*x2^8*x3^3 + 45*x1*x2^8*x3^2 + 41*x1*x2^8*x3 + 15*x1*x2^8 + 21*x1*x2^7*x3^12 + 40*x1*x2^7*x3^11 + 67*x1*x2^7*x3^10 + 53*x1*x2^7*x3^9 + 119*x1*x2^7*x3^8 + 122*x1*x2^7*x3^7 + 176*x1*x2^7*x3^6 + 118*x1*x2^7*x3^5 + 176*x1*x2^7*x3^4 + 90*x1*x2^7*x3^3 + 71*x1*x2^7*x3^2 + 40*x1*x2^7*x3 + 27*x1*x2^7 + 6*x1*x2^6*x3^12 + 34*x1*x2^6*x3^11 + 37*x1*x2^6*x3^10 + 93*x1*x2^6*x3^9 + 107*x1*x2^6*x3^8 + 176*x1*x2^6*x3^7 + 120*x1*x2^6*x3^6 + 194*x1*x2^6*x3^5 + 126*x1*x2^6*x3^4 + 140*x1*x2^6*x3^3 + 82*x1*x2^6*x3^2 + 71*x1*x2^6*x3 + 39*x1*x2^6 + 11*x1*x2^5*x3^12 + 20*x1*x2^5*x3^11 + 75*x1*x2^5*x3^10 + 80*x1*x2^5*x3^9 + 143*x1*x2^5*x3^8 + 118*x1*x2^5*x3^7 + 194*x1*x2^5*x3^6 + 135*x1*x2^5*x3^5 + 182*x1*x2^5*x3^4 + 129*x1*x2^5*x3^3 + 120*x1*x2^5*x3^2 + 55*x1*x2^5*x3 + 23*x1*x2^5 + 6*x1*x2^4*x3^12 + 50*x1*x2^4*x3^11 + 46*x1*x2^4*x3^10 + 115*x1*x2^4*x3^9 + 98*x1*x2^4*x3^8 + 176*x1*x2^4*x3^7 + 126*x1*x2^4*x3^6 + 182*x1*x2^4*x3^5 + 144*x1*x2^4*x3^4 + 150*x1*x2^4*x3^3 + 76*x1*x2^4*x3^2 + 46*x1*x2^4*x3 + 14*x1*x2^4 + 21*x1*x2^3*x3^12 + 12*x1*x2^3*x3^11 + 73*x1*x2^3*x3^10 + 55*x1*x2^3*x3^9 + 129*x1*x2^3*x3^8 + 90*x1*x2^3*x3^7 + 140*x1*x2^3*x3^6 + 129*x1*x2^3*x3^5 + 150*x1*x2^3*x3^4 + 90*x1*x2^3*x3^3 + 55*x1*x2^3*x3^2 + 39*x1*x2^3*x3 + 34*x1*x2^3 + 28*x1*x2^2*x3^11 + 21*x1*x2^2*x3^10 + 80*x1*x2^2*x3^9 + 45*x1*x2^2*x3^8 + 71*x1*x2^2*x3^7 + 82*x1*x2^2*x3^6 + 120*x1*x2^2*x3^5 + 76*x1*x2^2*x3^4 + 55*x1*x2^2*x3^3 + 50*x1*x2^2*x3^2 + 51*x1*x2^2*x3 + 33*x1*x2^2 + 6*x1*x2*x3^11 + 47*x1*x2*x3^10 + 26*x1*x2*x3^9 + 41*x1*x2*x3^8 + 40*x1*x2*x3^7 + 71*x1*x2*x3^6 + 55*x1*x2*x3^5 + 46*x1*x2*x3^4 + 39*x1*x2*x3^3 + 51*x1*x2*x3^2 + 65*x1*x2*x3 + 22*x1*x2 + 13*x1*x3^11 + 18*x1*x3^10 + 31*x1*x3^9 + 15*x1*x3^8 + 27*x1*x3^7 + 39*x1*x3^6 + 23*x1*x3^5 + 14*x1*x3^4 + 34*x1*x3^3 + 33*x1*x3^2 + 22*x1*x3 + 16*x1 + 21*x2^12*x3^8 + 6*x2^12*x3^7 + 11*x2^12*x3^6 + 6*x2^12*x3^5 + 21*x2^12*x3^4 + 11*x2^11*x3^11 + 13*x2^11*x3^10 + 27*x2^11*x3^9 + 34*x2^11*x3^8 + 23*x2^11*x3^7 + 14*x2^11*x3^6 + 29*x2^11*x3^5 + 12*x2^11*x3^4 + 28*x2^11*x3^3 + 6*x2^11*x3^2 + 13*x2^11*x3 + 11*x2^11 + 13*x2^10*x3^11 + 51*x2^10*x3^10 + 41*x2^10*x3^9 + 44*x2^10*x3^8 + 23*x2^10*x3^7 + 46*x2^10*x3^6 + 34*x2^10*x3^5 + 45*x2^10*x3^4 + 15*x2^10*x3^3 + 34*x2^10*x3^2 + 18*x2^10*x3 + 24*x2^10 + 27*x2^9*x3^11 + 41*x2^9*x3^10 + 44*x2^9*x3^9 + 30*x2^9*x3^8 + 47*x2^9*x3^7 + 46*x2^9*x3^6 + 70*x2^9*x3^5 + 40*x2^9*x3^4 + 46*x2^9*x3^3 + 19*x2^9*x3^2 + 31*x2^9*x3 + 21*x2^8*x3^12 + 34*x2^8*x3^11 + 44*x2^8*x3^10 + 30*x2^8*x3^9 + 72*x2^8*x3^8 + 61*x2^8*x3^7 + 73*x2^8*x3^6 + 58*x2^8*x3^5 + 83*x2^8*x3^4 + 37*x2^8*x3^3 + 34*x2^8*x3^2 + 15*x2^8*x3 + 25*x2^8 + 6*x2^7*x3^12 + 23*x2^7*x3^11 + 23*x2^7*x3^10 + 47*x2^7*x3^9 + 61*x2^7*x3^8 + 103*x2^7*x3^7 + 60*x2^7*x3^6 + 93*x2^7*x3^5 + 64*x2^7*x3^4 + 61*x2^7*x3^3 + 25*x2^7*x3^2 + 27*x2^7*x3 + 30*x2^7 + 11*x2^6*x3^12 + 14*x2^6*x3^11 + 46*x2^6*x3^10 + 46*x2^6*x3^9 + 73*x2^6*x3^8 + 60*x2^6*x3^7 + 101*x2^6*x3^6 + 73*x2^6*x3^5 + 103*x2^6*x3^4 + 57*x2^6*x3^3 + 69*x2^6*x3^2 + 39*x2^6*x3 + 8*x2^6 + 6*x2^5*x3^12 + 29*x2^5*x3^11 + 34*x2^5*x3^10 + 70*x2^5*x3^9 + 58*x2^5*x3^8 + 93*x2^5*x3^7 + 73*x2^5*x3^6 + 103*x2^5*x3^5 + 72*x2^5*x3^4 + 76*x2^5*x3^3 + 46*x2^5*x3^2 + 23*x2^5*x3 + 21*x2^4*x3^12 + 12*x2^4*x3^11 + 45*x2^4*x3^10 + 40*x2^4*x3^9 + 83*x2^4*x3^8 + 64*x2^4*x3^7 + 103*x2^4*x3^6 + 72*x2^4*x3^5 + 99*x2^4*x3^4 + 60*x2^4*x3^3 + 31*x2^4*x3^2 + 14*x2^4*x3 + 23*x2^4 + 28*x2^3*x3^11 + 15*x2^3*x3^10 + 46*x2^3*x3^9 + 37*x2^3*x3^8 + 61*x2^3*x3^7 + 57*x2^3*x3^6 + 76*x2^3*x3^5 + 60*x2^3*x3^4 + 32*x2^3*x3^3 + 25*x2^3*x3^2 + 34*x2^3*x3 + x2^3 + 6*x2^2*x3^11 + 34*x2^2*x3^10 + 19*x2^2*x3^9 + 34*x2^2*x3^8 + 25*x2^2*x3^7 + 69*x2^2*x3^6 + 46*x2^2*x3^5 + 31*x2^2*x3^4 + 25*x2^2*x3^3 + 40*x2^2*x3^2 + 33*x2^2*x3 + 6*x2^2 + 13*x2*x3^11 + 18*x2*x3^10 + 31*x2*x3^9 + 15*x2*x3^8 + 27*x2*x3^7 + 39*x2*x3^6 + 23*x2*x3^5 + 14*x2*x3^4 + 34*x2*x3^3 + 33*x2*x3^2 + 22*x2*x3 + 16*x2 + 11*x3^11 + 24*x3^10 + 25*x3^8 + 30*x3^7 + 8*x3^6 + 23*x3^4 + x3^3 + 6*x3^2 + 16*x3
==================
Q = dot_prod(sol_w, list_s) = 21*x1^10*x2^10 + 21*x1^10*x2^9*x3 + 6*x1^10*x2^9 + 21*x1^10*x2^8*x3^2 + 6*x1^10*x2^8*x3 + 11*x1^10*x2^8 + 21*x1^10*x2^7*x3^3 + 6*x1^10*x2^7*x3^2 + 11*x1^10*x2^7*x3 + 17*x1^10*x2^7 + 21*x1^10*x2^6*x3^4 + 6*x1^10*x2^6*x3^3 + 11*x1^10*x2^6*x3^2 + 17*x1^10*x2^6*x3 + 34*x1^10*x2^6 + 21*x1^10*x2^5*x3^5 + 6*x1^10*x2^5*x3^4 + 11*x1^10*x2^5*x3^3 + 17*x1^10*x2^5*x3^2 + 34*x1^10*x2^5*x3 + 27*x1^10*x2^5 + 21*x1^10*x2^4*x3^6 + 6*x1^10*x2^4*x3^5 + 11*x1^10*x2^4*x3^4 + 17*x1^10*x2^4*x3^3 + 34*x1^10*x2^4*x3^2 + 27*x1^10*x2^4*x3 + 34*x1^10*x2^4 + 21*x1^10*x2^3*x3^7 + 6*x1^10*x2^3*x3^6 + 11*x1^10*x2^3*x3^5 + 17*x1^10*x2^3*x3^4 + 34*x1^10*x2^3*x3^3 + 27*x1^10*x2^3*x3^2 + 34*x1^10*x2^3*x3 + 17*x1^10*x2^3 + 21*x1^10*x2^2*x3^8 + 6*x1^10*x2^2*x3^7 + 11*x1^10*x2^2*x3^6 + 17*x1^10*x2^2*x3^5 + 34*x1^10*x2^2*x3^4 + 27*x1^10*x2^2*x3^3 + 34*x1^10*x2^2*x3^2 + 17*x1^10*x2^2*x3 + 11*x1^10*x2^2 + 21*x1^10*x2*x3^9 + 6*x1^10*x2*x3^8 + 11*x1^10*x2*x3^7 + 17*x1^10*x2*x3^6 + 34*x1^10*x2*x3^5 + 27*x1^10*x2*x3^4 + 34*x1^10*x2*x3^3 + 17*x1^10*x2*x3^2 + 11*x1^10*x2*x3 + 6*x1^10*x2 + 21*x1^10*x3^10 + 6*x1^10*x3^9 + 11*x1^10*x3^8 + 17*x1^10*x3^7 + 34*x1^10*x3^6 + 27*x1^10*x3^5 + 34*x1^10*x3^4 + 17*x1^10*x3^3 + 11*x1^10*x3^2 + 6*x1^10*x3 + 21*x1^10 + 21*x1^9*x2^10*x3 + 6*x1^9*x2^10 + 21*x1^9*x2^9*x3^2 + 12*x1^9*x2^9*x3 + 24*x1^9*x2^9 + 21*x1^9*x2^8*x3^3 + 12*x1^9*x2^8*x3^2 + 35*x1^9*x2^8*x3 + 21*x1^9*x2^8 + 21*x1^9*x2^7*x3^4 + 12*x1^9*x2^7*x3^3 + 35*x1^9*x2^7*x3^2 + 38*x1^9*x2^7*x3 + 47*x1^9*x2^7 + 21*x1^9*x2^6*x3^5 + 12*x1^9*x2^6*x3^4 + 35*x1^9*x2^6*x3^3 + 38*x1^9*x2^6*x3^2 + 81*x1^9*x2^6*x3 + 75*x1^9*x2^6 + 21*x1^9*x2^5*x3^6 + 12*x1^9*x2^5*x3^5 + 35*x1^9*x2^5*x3^4 + 38*x1^9*x2^5*x3^3 + 81*x1^9*x2^5*x3^2 + 102*x1^9*x2^5*x3 + 67*x1^9*x2^5 + 21*x1^9*x2^4*x3^7 + 12*x1^9*x2^4*x3^6 + 35*x1^9*x2^4*x3^5 + 38*x1^9*x2^4*x3^4 + 81*x1^9*x2^4*x3^3 + 102*x1^9*x2^4*x3^2 + 101*x1^9*x2^4*x3 + 50*x1^9*x2^4 + 21*x1^9*x2^3*x3^8 + 12*x1^9*x2^3*x3^7 + 35*x1^9*x2^3*x3^6 + 38*x1^9*x2^3*x3^5 + 81*x1^9*x2^3*x3^4 + 102*x1^9*x2^3*x3^3 + 101*x1^9*x2^3*x3^2 + 67*x1^9*x2^3*x3 + 59*x1^9*x2^3 + 21*x1^9*x2^2*x3^9 + 12*x1^9*x2^2*x3^8 + 35*x1^9*x2^2*x3^7 + 38*x1^9*x2^2*x3^6 + 81*x1^9*x2^2*x3^5 + 102*x1^9*x2^2*x3^4 + 101*x1^9*x2^2*x3^3 + 67*x1^9*x2^2*x3^2 + 70*x1^9*x2^2*x3 + 19*x1^9*x2^2 + 21*x1^9*x2*x3^10 + 12*x1^9*x2*x3^9 + 35*x1^9*x2*x3^8 + 38*x1^9*x2*x3^7 + 81*x1^9*x2*x3^6 + 102*x1^9*x2*x3^5 + 101*x1^9*x2*x3^4 + 67*x1^9*x2*x3^3 + 70*x1^9*x2*x3^2 + 25*x1^9*x2*x3 + 25*x1^9*x2 + 6*x1^9*x3^10 + 24*x1^9*x3^9 + 21*x1^9*x3^8 + 47*x1^9*x3^7 + 75*x1^9*x3^6 + 67*x1^9*x3^5 + 50*x1^9*x3^4 + 59*x1^9*x3^3 + 19*x1^9*x3^2 + 25*x1^9*x3 + 13*x1^9 + 21*x1^8*x2^10*x3^2 + 6*x1^8*x2^10*x3 + 11*x1^8*x2^10 + 21*x1^8*x2^9*x3^3 + 12*x1^8*x2^9*x3^2 + 35*x1^8*x2^9*x3 + 21*x1^8*x2^9 + 21*x1^8*x2^8*x3^4 + 12*x1^8*x2^8*x3^3 + 46*x1^8*x2^8*x3^2 + 42*x1^8*x2^8*x3 + 84*x1^8*x2^8 + 21*x1^8*x2^7*x3^5 + 12*x1^8*x2^7*x3^4 + 46*x1^8*x2^7*x3^3 + 59*x1^8*x2^7*x3^2 + 131*x1^8*x2^7*x3 + 82*x1^8*x2^7 + 21*x1^8*x2^6*x3^6 + 12*x1^8*x2^6*x3^5 + 46*x1^8*x2^6*x3^4 + 59*x1^8*x2^6*x3^3 + 165*x1^8*x2^6*x3^2 + 157*x1^8*x2^6*x3 + 100*x1^8*x2^6 + 21*x1^8*x2^5*x3^7 + 12*x1^8*x2^5*x3^6 + 46*x1^8*x2^5*x3^5 + 59*x1^8*x2^5*x3^4 + 165*x1^8*x2^5*x3^3 + 184*x1^8*x2^5*x3^2 + 167*x1^8*x2^5*x3 + 98*x1^8*x2^5 + 21*x1^8*x2^4*x3^8 + 12*x1^8*x2^4*x3^7 + 46*x1^8*x2^4*x3^6 + 59*x1^8*x2^4*x3^5 + 165*x1^8*x2^4*x3^4 + 184*x1^8*x2^4*x3^3 + 201*x1^8*x2^4*x3^2 + 148*x1^8*x2^4*x3 + 85*x1^8*x2^4 + 21*x1^8*x2^3*x3^9 + 12*x1^8*x2^3*x3^8 + 46*x1^8*x2^3*x3^7 + 59*x1^8*x2^3*x3^6 + 165*x1^8*x2^3*x3^5 + 184*x1^8*x2^3*x3^4 + 201*x1^8*x2^3*x3^3 + 165*x1^8*x2^3*x3^2 + 144*x1^8*x2^3*x3 + 67*x1^8*x2^3 + 21*x1^8*x2^2*x3^10 + 12*x1^8*x2^2*x3^9 + 46*x1^8*x2^2*x3^8 + 59*x1^8*x2^2*x3^7 + 165*x1^8*x2^2*x3^6 + 184*x1^8*x2^2*x3^5 + 201*x1^8*x2^2*x3^4 + 165*x1^8*x2^2*x3^3 + 155*x1^8*x2^2*x3^2 + 86*x1^8*x2^2*x3 + 58*x1^8*x2^2 + 6*x1^8*x2*x3^10 + 35*x1^8*x2*x3^9 + 42*x1^8*x2*x3^8 + 131*x1^8*x2*x3^7 + 157*x1^8*x2*x3^6 + 167*x1^8*x2*x3^5 + 148*x1^8*x2*x3^4 + 144*x1^8*x2*x3^3 + 86*x1^8*x2*x3^2 + 62*x1^8*x2*x3 + 20*x1^8*x2 + 11*x1^8*x3^10 + 21*x1^8*x3^9 + 84*x1^8*x3^8 + 82*x1^8*x3^7 + 100*x1^8*x3^6 + 98*x1^8*x3^5 + 85*x1^8*x3^4 + 67*x1^8*x3^3 + 58*x1^8*x3^2 + 20*x1^8*x3 + 37*x1^8 + 21*x1^7*x2^10*x3^3 + 6*x1^7*x2^10*x3^2 + 11*x1^7*x2^10*x3 + 17*x1^7*x2^10 + 21*x1^7*x2^9*x3^4 + 12*x1^7*x2^9*x3^3 + 35*x1^7*x2^9*x3^2 + 38*x1^7*x2^9*x3 + 47*x1^7*x2^9 + 21*x1^7*x2^8*x3^5 + 12*x1^7*x2^8*x3^4 + 46*x1^7*x2^8*x3^3 + 59*x1^7*x2^8*x3^2 + 131*x1^7*x2^8*x3 + 82*x1^7*x2^8 + 21*x1^7*x2^7*x3^6 + 12*x1^7*x2^7*x3^5 + 46*x1^7*x2^7*x3^4 + 76*x1^7*x2^7*x3^3 + 178*x1^7*x2^7*x3^2 + 164*x1^7*x2^7*x3 + 139*x1^7*x2^7 + 21*x1^7*x2^6*x3^7 + 12*x1^7*x2^6*x3^6 + 46*x1^7*x2^6*x3^5 + 76*x1^7*x2^6*x3^4 + 212*x1^7*x2^6*x3^3 + 239*x1^7*x2^6*x3^2 + 239*x1^7*x2^6*x3 + 98*x1^7*x2^6 + 21*x1^7*x2^5*x3^8 + 12*x1^7*x2^5*x3^7 + 46*x1^7*x2^5*x3^6 + 76*x1^7*x2^5*x3^5 + 212*x1^7*x2^5*x3^4 + 266*x1^7*x2^5*x3^3 + 306*x1^7*x2^5*x3^2 + 196*x1^7*x2^5*x3 + 98*x1^7*x2^5 + 21*x1^7*x2^4*x3^9 + 12*x1^7*x2^4*x3^8 + 46*x1^7*x2^4*x3^7 + 76*x1^7*x2^4*x3^6 + 212*x1^7*x2^4*x3^5 + 266*x1^7*x2^4*x3^4 + 340*x1^7*x2^4*x3^3 + 246*x1^7*x2^4*x3^2 + 183*x1^7*x2^4*x3 + 92*x1^7*x2^4 + 21*x1^7*x2^3*x3^10 + 12*x1^7*x2^3*x3^9 + 46*x1^7*x2^3*x3^8 + 76*x1^7*x2^3*x3^7 + 212*x1^7*x2^3*x3^6 + 266*x1^7*x2^3*x3^5 + 340*x1^7*x2^3*x3^4 + 263*x1^7*x2^3*x3^3 + 242*x1^7*x2^3*x3^2 + 159*x1^7*x2^3*x3 + 83*x1^7*x2^3 + 6*x1^7*x2^2*x3^10 + 35*x1^7*x2^2*x3^9 + 59*x1^7*x2^2*x3^8 + 178*x1^7*x2^2*x3^7 + 239*x1^7*x2^2*x3^6 + 306*x1^7*x2^2*x3^5 + 246*x1^7*x2^2*x3^4 + 242*x1^7*x2^2*x3^3 + 172*x1^7*x2^2*x3^2 + 120*x1^7*x2^2*x3 + 33*x1^7*x2^2 + 11*x1^7*x2*x3^10 + 38*x1^7*x2*x3^9 + 131*x1^7*x2*x3^8 + 164*x1^7*x2*x3^7 + 239*x1^7*x2*x3^6 + 196*x1^7*x2*x3^5 + 183*x1^7*x2*x3^4 + 159*x1^7*x2*x3^3 + 120*x1^7*x2*x3^2 + 40*x1^7*x2*x3 + 37*x1^7*x2 + 17*x1^7*x3^10 + 47*x1^7*x3^9 + 82*x1^7*x3^8 + 139*x1^7*x3^7 + 98*x1^7*x3^6 + 98*x1^7*x3^5 + 92*x1^7*x3^4 + 83*x1^7*x3^3 + 33*x1^7*x3^2 + 37*x1^7*x3 + 39*x1^7 + 21*x1^6*x2^10*x3^4 + 6*x1^6*x2^10*x3^3 + 11*x1^6*x2^10*x3^2 + 17*x1^6*x2^10*x3 + 34*x1^6*x2^10 + 21*x1^6*x2^9*x3^5 + 12*x1^6*x2^9*x3^4 + 35*x1^6*x2^9*x3^3 + 38*x1^6*x2^9*x3^2 + 81*x1^6*x2^9*x3 + 75*x1^6*x2^9 + 21*x1^6*x2^8*x3^6 + 12*x1^6*x2^8*x3^5 + 46*x1^6*x2^8*x3^4 + 59*x1^6*x2^8*x3^3 + 165*x1^6*x2^8*x3^2 + 157*x1^6*x2^8*x3 + 100*x1^6*x2^8 + 21*x1^6*x2^7*x3^7 + 12*x1^6*x2^7*x3^6 + 46*x1^6*x2^7*x3^5 + 76*x1^6*x2^7*x3^4 + 212*x1^6*x2^7*x3^3 + 239*x1^6*x2^7*x3^2 + 239*x1^6*x2^7*x3 + 98*x1^6*x2^7 + 21*x1^6*x2^6*x3^8 + 12*x1^6*x2^6*x3^7 + 46*x1^6*x2^6*x3^6 + 76*x1^6*x2^6*x3^5 + 246*x1^6*x2^6*x3^4 + 314*x1^6*x2^6*x3^3 + 339*x1^6*x2^6*x3^2 + 196*x1^6*x2^6*x3 + 155*x1^6*x2^6 + 21*x1^6*x2^5*x3^9 + 12*x1^6*x2^5*x3^8 + 46*x1^6*x2^5*x3^7 + 76*x1^6*x2^5*x3^6 + 246*x1^6*x2^5*x3^5 + 341*x1^6*x2^5*x3^4 + 406*x1^6*x2^5*x3^3 + 294*x1^6*x2^5*x3^2 + 253*x1^6*x2^5*x3 + 108*x1^6*x2^5 + 21*x1^6*x2^4*x3^10 + 12*x1^6*x2^4*x3^9 + 46*x1^6*x2^4*x3^8 + 76*x1^6*x2^4*x3^7 + 246*x1^6*x2^4*x3^6 + 341*x1^6*x2^4*x3^5 + 440*x1^6*x2^4*x3^4 + 344*x1^6*x2^4*x3^3 + 338*x1^6*x2^4*x3^2 + 200*x1^6*x2^4*x3 + 126*x1^6*x2^4 + 6*x1^6*x2^3*x3^10 + 35*x1^6*x2^3*x3^9 + 59*x1^6*x2^3*x3^8 + 212*x1^6*x2^3*x3^7 + 314*x1^6*x2^3*x3^6 + 406*x1^6*x2^3*x3^5 + 344*x1^6*x2^3*x3^4 + 386*x1^6*x2^3*x3^3 + 261*x1^6*x2^3*x3^2 + 188*x1^6*x2^3*x3 + 104*x1^6*x2^3 + 11*x1^6*x2^2*x3^10 + 38*x1^6*x2^2*x3^9 + 165*x1^6*x2^2*x3^8 + 239*x1^6*x2^2*x3^7 + 339*x1^6*x2^2*x3^6 + 294*x1^6*x2^2*x3^5 + 338*x1^6*x2^2*x3^4 + 261*x1^6*x2^2*x3^3 + 221*x1^6*x2^2*x3^2 + 124*x1^6*x2^2*x3 + 80*x1^6*x2^2 + 17*x1^6*x2*x3^10 + 81*x1^6*x2*x3^9 + 157*x1^6*x2*x3^8 + 239*x1^6*x2*x3^7 + 196*x1^6*x2*x3^6 + 253*x1^6*x2*x3^5 + 200*x1^6*x2*x3^4 + 188*x1^6*x2*x3^3 + 124*x1^6*x2*x3^2 + 80*x1^6*x2*x3 + 55*x1^6*x2 + 34*x1^6*x3^10 + 75*x1^6*x3^9 + 100*x1^6*x3^8 + 98*x1^6*x3^7 + 155*x1^6*x3^6 + 108*x1^6*x3^5 + 126*x1^6*x3^4 + 104*x1^6*x3^3 + 80*x1^6*x3^2 + 55*x1^6*x3 + 57*x1^6 + 21*x1^5*x2^10*x3^5 + 6*x1^5*x2^10*x3^4 + 11*x1^5*x2^10*x3^3 + 17*x1^5*x2^10*x3^2 + 34*x1^5*x2^10*x3 + 27*x1^5*x2^10 + 21*x1^5*x2^9*x3^6 + 12*x1^5*x2^9*x3^5 + 35*x1^5*x2^9*x3^4 + 38*x1^5*x2^9*x3^3 + 81*x1^5*x2^9*x3^2 + 102*x1^5*x2^9*x3 + 67*x1^5*x2^9 + 21*x1^5*x2^8*x3^7 + 12*x1^5*x2^8*x3^6 + 46*x1^5*x2^8*x3^5 + 59*x1^5*x2^8*x3^4 + 165*x1^5*x2^8*x3^3 + 184*x1^5*x2^8*x3^2 + 167*x1^5*x2^8*x3 + 98*x1^5*x2^8 + 21*x1^5*x2^7*x3^8 + 12*x1^5*x2^7*x3^7 + 46*x1^5*x2^7*x3^6 + 76*x1^5*x2^7*x3^5 + 212*x1^5*x2^7*x3^4 + 266*x1^5*x2^7*x3^3 + 306*x1^5*x2^7*x3^2 + 196*x1^5*x2^7*x3 + 98*x1^5*x2^7 + 21*x1^5*x2^6*x3^9 + 12*x1^5*x2^6*x3^8 + 46*x1^5*x2^6*x3^7 + 76*x1^5*x2^6*x3^6 + 246*x1^5*x2^6*x3^5 + 341*x1^5*x2^6*x3^4 + 406*x1^5*x2^6*x3^3 + 294*x1^5*x2^6*x3^2 + 253*x1^5*x2^6*x3 + 108*x1^5*x2^6 + 21*x1^5*x2^5*x3^10 + 12*x1^5*x2^5*x3^9 + 46*x1^5*x2^5*x3^8 + 76*x1^5*x2^5*x3^7 + 246*x1^5*x2^5*x3^6 + 368*x1^5*x2^5*x3^5 + 473*x1^5*x2^5*x3^4 + 392*x1^5*x2^5*x3^3 + 351*x1^5*x2^5*x3^2 + 216*x1^5*x2^5*x3 + 175*x1^5*x2^5 + 6*x1^5*x2^4*x3^10 + 35*x1^5*x2^4*x3^9 + 59*x1^5*x2^4*x3^8 + 212*x1^5*x2^4*x3^7 + 341*x1^5*x2^4*x3^6 + 473*x1^5*x2^4*x3^5 + 425*x1^5*x2^4*x3^4 + 425*x1^5*x2^4*x3^3 + 302*x1^5*x2^4*x3^2 + 280*x1^5*x2^4*x3 + 124*x1^5*x2^4 + 11*x1^5*x2^3*x3^10 + 38*x1^5*x2^3*x3^9 + 165*x1^5*x2^3*x3^8 + 266*x1^5*x2^3*x3^7 + 406*x1^5*x2^3*x3^6 + 392*x1^5*x2^3*x3^5 + 425*x1^5*x2^3*x3^4 + 350*x1^5*x2^3*x3^3 + 338*x1^5*x2^3*x3^2 + 215*x1^5*x2^3*x3 + 131*x1^5*x2^3 + 17*x1^5*x2^2*x3^10 + 81*x1^5*x2^2*x3^9 + 184*x1^5*x2^2*x3^8 + 306*x1^5*x2^2*x3^7 + 294*x1^5*x2^2*x3^6 + 351*x1^5*x2^2*x3^5 + 302*x1^5*x2^2*x3^4 + 338*x1^5*x2^2*x3^3 + 228*x1^5*x2^2*x3^2 + 174*x1^5*x2^2*x3 + 106*x1^5*x2^2 + 34*x1^5*x2*x3^10 + 102*x1^5*x2*x3^9 + 167*x1^5*x2*x3^8 + 196*x1^5*x2*x3^7 + 253*x1^5*x2*x3^6 + 216*x1^5*x2*x3^5 + 280*x1^5*x2*x3^4 + 215*x1^5*x2*x3^3 + 174*x1^5*x2*x3^2 + 122*x1^5*x2*x3 + 77*x1^5*x2 + 27*x1^5*x3^10 + 67*x1^5*x3^9 + 98*x1^5*x3^8 + 98*x1^5*x3^7 + 108*x1^5*x3^6 + 175*x1^5*x3^5 + 124*x1^5*x3^4 + 131*x1^5*x3^3 + 106*x1^5*x3^2 + 77*x1^5*x3 + 49*x1^5 + 21*x1^4*x2^10*x3^6 + 6*x1^4*x2^10*x3^5 + 11*x1^4*x2^10*x3^4 + 17*x1^4*x2^10*x3^3 + 34*x1^4*x2^10*x3^2 + 27*x1^4*x2^10*x3 + 34*x1^4*x2^10 + 21*x1^4*x2^9*x3^7 + 12*x1^4*x2^9*x3^6 + 35*x1^4*x2^9*x3^5 + 38*x1^4*x2^9*x3^4 + 81*x1^4*x2^9*x3^3 + 102*x1^4*x2^9*x3^2 + 101*x1^4*x2^9*x3 + 50*x1^4*x2^9 + 21*x1^4*x2^8*x3^8 + 12*x1^4*x2^8*x3^7 + 46*x1^4*x2^8*x3^6 + 59*x1^4*x2^8*x3^5 + 165*x1^4*x2^8*x3^4 + 184*x1^4*x2^8*x3^3 + 201*x1^4*x2^8*x3^2 + 148*x1^4*x2^8*x3 + 85*x1^4*x2^8 + 21*x1^4*x2^7*x3^9 + 12*x1^4*x2^7*x3^8 + 46*x1^4*x2^7*x3^7 + 76*x1^4*x2^7*x3^6 + 212*x1^4*x2^7*x3^5 + 266*x1^4*x2^7*x3^4 + 340*x1^4*x2^7*x3^3 + 246*x1^4*x2^7*x3^2 + 183*x1^4*x2^7*x3 + 92*x1^4*x2^7 + 21*x1^4*x2^6*x3^10 + 12*x1^4*x2^6*x3^9 + 46*x1^4*x2^6*x3^8 + 76*x1^4*x2^6*x3^7 + 246*x1^4*x2^6*x3^6 + 341*x1^4*x2^6*x3^5 + 440*x1^4*x2^6*x3^4 + 344*x1^4*x2^6*x3^3 + 338*x1^4*x2^6*x3^2 + 200*x1^4*x2^6*x3 + 126*x1^4*x2^6 + 6*x1^4*x2^5*x3^10 + 35*x1^4*x2^5*x3^9 + 59*x1^4*x2^5*x3^8 + 212*x1^4*x2^5*x3^7 + 341*x1^4*x2^5*x3^6 + 473*x1^4*x2^5*x3^5 + 425*x1^4*x2^5*x3^4 + 425*x1^4*x2^5*x3^3 + 302*x1^4*x2^5*x3^2 + 280*x1^4*x2^5*x3 + 124*x1^4*x2^5 + 11*x1^4*x2^4*x3^10 + 38*x1^4*x2^4*x3^9 + 165*x1^4*x2^4*x3^8 + 266*x1^4*x2^4*x3^7 + 440*x1^4*x2^4*x3^6 + 425*x1^4*x2^4*x3^5 + 451*x1^4*x2^4*x3^4 + 375*x1^4*x2^4*x3^3 + 381*x1^4*x2^4*x3^2 + 235*x1^4*x2^4*x3 + 174*x1^4*x2^4 + 17*x1^4*x2^3*x3^10 + 81*x1^4*x2^3*x3^9 + 184*x1^4*x2^3*x3^8 + 340*x1^4*x2^3*x3^7 + 344*x1^4*x2^3*x3^6 + 425*x1^4*x2^3*x3^5 + 375*x1^4*x2^3*x3^4 + 406*x1^4*x2^3*x3^3 + 319*x1^4*x2^3*x3^2 + 268*x1^4*x2^3*x3 + 124*x1^4*x2^3 + 34*x1^4*x2^2*x3^10 + 102*x1^4*x2^2*x3^9 + 201*x1^4*x2^2*x3^8 + 246*x1^4*x2^2*x3^7 + 338*x1^4*x2^2*x3^6 + 302*x1^4*x2^2*x3^5 + 381*x1^4*x2^2*x3^4 + 319*x1^4*x2^2*x3^3 + 311*x1^4*x2^2*x3^2 + 191*x1^4*x2^2*x3 + 102*x1^4*x2^2 + 27*x1^4*x2*x3^10 + 101*x1^4*x2*x3^9 + 148*x1^4*x2*x3^8 + 183*x1^4*x2*x3^7 + 200*x1^4*x2*x3^6 + 280*x1^4*x2*x3^5 + 235*x1^4*x2*x3^4 + 268*x1^4*x2*x3^3 + 191*x1^4*x2*x3^2 + 122*x1^4*x2*x3 + 67*x1^4*x2 + 34*x1^4*x3^10 + 50*x1^4*x3^9 + 85*x1^4*x3^8 + 92*x1^4*x3^7 + 126*x1^4*x3^6 + 124*x1^4*x3^5 + 174*x1^4*x3^4 + 124*x1^4*x3^3 + 102*x1^4*x3^2 + 67*x1^4*x3 + 43*x1^4 + 21*x1^3*x2^10*x3^7 + 6*x1^3*x2^10*x3^6 + 11*x1^3*x2^10*x3^5 + 17*x1^3*x2^10*x3^4 + 34*x1^3*x2^10*x3^3 + 27*x1^3*x2^10*x3^2 + 34*x1^3*x2^10*x3 + 17*x1^3*x2^10 + 21*x1^3*x2^9*x3^8 + 12*x1^3*x2^9*x3^7 + 35*x1^3*x2^9*x3^6 + 38*x1^3*x2^9*x3^5 + 81*x1^3*x2^9*x3^4 + 102*x1^3*x2^9*x3^3 + 101*x1^3*x2^9*x3^2 + 67*x1^3*x2^9*x3 + 59*x1^3*x2^9 + 21*x1^3*x2^8*x3^9 + 12*x1^3*x2^8*x3^8 + 46*x1^3*x2^8*x3^7 + 59*x1^3*x2^8*x3^6 + 165*x1^3*x2^8*x3^5 + 184*x1^3*x2^8*x3^4 + 201*x1^3*x2^8*x3^3 + 165*x1^3*x2^8*x3^2 + 144*x1^3*x2^8*x3 + 67*x1^3*x2^8 + 21*x1^3*x2^7*x3^10 + 12*x1^3*x2^7*x3^9 + 46*x1^3*x2^7*x3^8 + 76*x1^3*x2^7*x3^7 + 212*x1^3*x2^7*x3^6 + 266*x1^3*x2^7*x3^5 + 340*x1^3*x2^7*x3^4 + 263*x1^3*x2^7*x3^3 + 242*x1^3*x2^7*x3^2 + 159*x1^3*x2^7*x3 + 83*x1^3*x2^7 + 6*x1^3*x2^6*x3^10 + 35*x1^3*x2^6*x3^9 + 59*x1^3*x2^6*x3^8 + 212*x1^3*x2^6*x3^7 + 314*x1^3*x2^6*x3^6 + 406*x1^3*x2^6*x3^5 + 344*x1^3*x2^6*x3^4 + 386*x1^3*x2^6*x3^3 + 261*x1^3*x2^6*x3^2 + 188*x1^3*x2^6*x3 + 104*x1^3*x2^6 + 11*x1^3*x2^5*x3^10 + 38*x1^3*x2^5*x3^9 + 165*x1^3*x2^5*x3^8 + 266*x1^3*x2^5*x3^7 + 406*x1^3*x2^5*x3^6 + 392*x1^3*x2^5*x3^5 + 425*x1^3*x2^5*x3^4 + 350*x1^3*x2^5*x3^3 + 338*x1^3*x2^5*x3^2 + 215*x1^3*x2^5*x3 + 131*x1^3*x2^5 + 17*x1^3*x2^4*x3^10 + 81*x1^3*x2^4*x3^9 + 184*x1^3*x2^4*x3^8 + 340*x1^3*x2^4*x3^7 + 344*x1^3*x2^4*x3^6 + 425*x1^3*x2^4*x3^5 + 375*x1^3*x2^4*x3^4 + 406*x1^3*x2^4*x3^3 + 319*x1^3*x2^4*x3^2 + 268*x1^3*x2^4*x3 + 124*x1^3*x2^4 + 34*x1^3*x2^3*x3^10 + 102*x1^3*x2^3*x3^9 + 201*x1^3*x2^3*x3^8 + 263*x1^3*x2^3*x3^7 + 386*x1^3*x2^3*x3^6 + 350*x1^3*x2^3*x3^5 + 406*x1^3*x2^3*x3^4 + 390*x1^3*x2^3*x3^3 + 362*x1^3*x2^3*x3^2 + 209*x1^3*x2^3*x3 + 138*x1^3*x2^3 + 27*x1^3*x2^2*x3^10 + 101*x1^3*x2^2*x3^9 + 165*x1^3*x2^2*x3^8 + 242*x1^3*x2^2*x3^7 + 261*x1^3*x2^2*x3^6 + 338*x1^3*x2^2*x3^5 + 319*x1^3*x2^2*x3^4 + 362*x1^3*x2^2*x3^3 + 260*x1^3*x2^2*x3^2 + 183*x1^3*x2^2*x3 + 109*x1^3*x2^2 + 34*x1^3*x2*x3^10 + 67*x1^3*x2*x3^9 + 144*x1^3*x2*x3^8 + 159*x1^3*x2*x3^7 + 188*x1^3*x2*x3^6 + 215*x1^3*x2*x3^5 + 268*x1^3*x2*x3^4 + 209*x1^3*x2*x3^3 + 183*x1^3*x2*x3^2 + 127*x1^3*x2*x3 + 85*x1^3*x2 + 17*x1^3*x3^10 + 59*x1^3*x3^9 + 67*x1^3*x3^8 + 83*x1^3*x3^7 + 104*x1^3*x3^6 + 131*x1^3*x3^5 + 124*x1^3*x3^4 + 138*x1^3*x3^3 + 109*x1^3*x3^2 + 85*x1^3*x3 + 36*x1^3 + 21*x1^2*x2^10*x3^8 + 6*x1^2*x2^10*x3^7 + 11*x1^2*x2^10*x3^6 + 17*x1^2*x2^10*x3^5 + 34*x1^2*x2^10*x3^4 + 27*x1^2*x2^10*x3^3 + 34*x1^2*x2^10*x3^2 + 17*x1^2*x2^10*x3 + 11*x1^2*x2^10 + 21*x1^2*x2^9*x3^9 + 12*x1^2*x2^9*x3^8 + 35*x1^2*x2^9*x3^7 + 38*x1^2*x2^9*x3^6 + 81*x1^2*x2^9*x3^5 + 102*x1^2*x2^9*x3^4 + 101*x1^2*x2^9*x3^3 + 67*x1^2*x2^9*x3^2 + 70*x1^2*x2^9*x3 + 19*x1^2*x2^9 + 21*x1^2*x2^8*x3^10 + 12*x1^2*x2^8*x3^9 + 46*x1^2*x2^8*x3^8 + 59*x1^2*x2^8*x3^7 + 165*x1^2*x2^8*x3^6 + 184*x1^2*x2^8*x3^5 + 201*x1^2*x2^8*x3^4 + 165*x1^2*x2^8*x3^3 + 155*x1^2*x2^8*x3^2 + 86*x1^2*x2^8*x3 + 58*x1^2*x2^8 + 6*x1^2*x2^7*x3^10 + 35*x1^2*x2^7*x3^9 + 59*x1^2*x2^7*x3^8 + 178*x1^2*x2^7*x3^7 + 239*x1^2*x2^7*x3^6 + 306*x1^2*x2^7*x3^5 + 246*x1^2*x2^7*x3^4 + 242*x1^2*x2^7*x3^3 + 172*x1^2*x2^7*x3^2 + 120*x1^2*x2^7*x3 + 33*x1^2*x2^7 + 11*x1^2*x2^6*x3^10 + 38*x1^2*x2^6*x3^9 + 165*x1^2*x2^6*x3^8 + 239*x1^2*x2^6*x3^7 + 339*x1^2*x2^6*x3^6 + 294*x1^2*x2^6*x3^5 + 338*x1^2*x2^6*x3^4 + 261*x1^2*x2^6*x3^3 + 221*x1^2*x2^6*x3^2 + 124*x1^2*x2^6*x3 + 80*x1^2*x2^6 + 17*x1^2*x2^5*x3^10 + 81*x1^2*x2^5*x3^9 + 184*x1^2*x2^5*x3^8 + 306*x1^2*x2^5*x3^7 + 294*x1^2*x2^5*x3^6 + 351*x1^2*x2^5*x3^5 + 302*x1^2*x2^5*x3^4 + 338*x1^2*x2^5*x3^3 + 228*x1^2*x2^5*x3^2 + 174*x1^2*x2^5*x3 + 106*x1^2*x2^5 + 34*x1^2*x2^4*x3^10 + 102*x1^2*x2^4*x3^9 + 201*x1^2*x2^4*x3^8 + 246*x1^2*x2^4*x3^7 + 338*x1^2*x2^4*x3^6 + 302*x1^2*x2^4*x3^5 + 381*x1^2*x2^4*x3^4 + 319*x1^2*x2^4*x3^3 + 311*x1^2*x2^4*x3^2 + 191*x1^2*x2^4*x3 + 102*x1^2*x2^4 + 27*x1^2*x2^3*x3^10 + 101*x1^2*x2^3*x3^9 + 165*x1^2*x2^3*x3^8 + 242*x1^2*x2^3*x3^7 + 261*x1^2*x2^3*x3^6 + 338*x1^2*x2^3*x3^5 + 319*x1^2*x2^3*x3^4 + 362*x1^2*x2^3*x3^3 + 260*x1^2*x2^3*x3^2 + 183*x1^2*x2^3*x3 + 109*x1^2*x2^3 + 34*x1^2*x2^2*x3^10 + 67*x1^2*x2^2*x3^9 + 155*x1^2*x2^2*x3^8 + 172*x1^2*x2^2*x3^7 + 221*x1^2*x2^2*x3^6 + 228*x1^2*x2^2*x3^5 + 311*x1^2*x2^2*x3^4 + 260*x1^2*x2^2*x3^3 + 208*x1^2*x2^2*x3^2 + 169*x1^2*x2^2*x3 + 95*x1^2*x2^2 + 17*x1^2*x2*x3^10 + 70*x1^2*x2*x3^9 + 86*x1^2*x2*x3^8 + 120*x1^2*x2*x3^7 + 124*x1^2*x2*x3^6 + 174*x1^2*x2*x3^5 + 191*x1^2*x2*x3^4 + 183*x1^2*x2*x3^3 + 169*x1^2*x2*x3^2 + 137*x1^2*x2*x3 + 55*x1^2*x2 + 11*x1^2*x3^10 + 19*x1^2*x3^9 + 58*x1^2*x3^8 + 33*x1^2*x3^7 + 80*x1^2*x3^6 + 106*x1^2*x3^5 + 102*x1^2*x3^4 + 109*x1^2*x3^3 + 95*x1^2*x3^2 + 55*x1^2*x3 + 10*x1^2 + 21*x1*x2^10*x3^9 + 6*x1*x2^10*x3^8 + 11*x1*x2^10*x3^7 + 17*x1*x2^10*x3^6 + 34*x1*x2^10*x3^5 + 27*x1*x2^10*x3^4 + 34*x1*x2^10*x3^3 + 17*x1*x2^10*x3^2 + 11*x1*x2^10*x3 + 6*x1*x2^10 + 21*x1*x2^9*x3^10 + 12*x1*x2^9*x3^9 + 35*x1*x2^9*x3^8 + 38*x1*x2^9*x3^7 + 81*x1*x2^9*x3^6 + 102*x1*x2^9*x3^5 + 101*x1*x2^9*x3^4 + 67*x1*x2^9*x3^3 + 70*x1*x2^9*x3^2 + 25*x1*x2^9*x3 + 25*x1*x2^9 + 6*x1*x2^8*x3^10 + 35*x1*x2^8*x3^9 + 42*x1*x2^8*x3^8 + 131*x1*x2^8*x3^7 + 157*x1*x2^8*x3^6 + 167*x1*x2^8*x3^5 + 148*x1*x2^8*x3^4 + 144*x1*x2^8*x3^3 + 86*x1*x2^8*x3^2 + 62*x1*x2^8*x3 + 20*x1*x2^8 + 11*x1*x2^7*x3^10 + 38*x1*x2^7*x3^9 + 131*x1*x2^7*x3^8 + 164*x1*x2^7*x3^7 + 239*x1*x2^7*x3^6 + 196*x1*x2^7*x3^5 + 183*x1*x2^7*x3^4 + 159*x1*x2^7*x3^3 + 120*x1*x2^7*x3^2 + 40*x1*x2^7*x3 + 37*x1*x2^7 + 17*x1*x2^6*x3^10 + 81*x1*x2^6*x3^9 + 157*x1*x2^6*x3^8 + 239*x1*x2^6*x3^7 + 196*x1*x2^6*x3^6 + 253*x1*x2^6*x3^5 + 200*x1*x2^6*x3^4 + 188*x1*x2^6*x3^3 + 124*x1*x2^6*x3^2 + 80*x1*x2^6*x3 + 55*x1*x2^6 + 34*x1*x2^5*x3^10 + 102*x1*x2^5*x3^9 + 167*x1*x2^5*x3^8 + 196*x1*x2^5*x3^7 + 253*x1*x2^5*x3^6 + 216*x1*x2^5*x3^5 + 280*x1*x2^5*x3^4 + 215*x1*x2^5*x3^3 + 174*x1*x2^5*x3^2 + 122*x1*x2^5*x3 + 77*x1*x2^5 + 27*x1*x2^4*x3^10 + 101*x1*x2^4*x3^9 + 148*x1*x2^4*x3^8 + 183*x1*x2^4*x3^7 + 200*x1*x2^4*x3^6 + 280*x1*x2^4*x3^5 + 235*x1*x2^4*x3^4 + 268*x1*x2^4*x3^3 + 191*x1*x2^4*x3^2 + 122*x1*x2^4*x3 + 67*x1*x2^4 + 34*x1*x2^3*x3^10 + 67*x1*x2^3*x3^9 + 144*x1*x2^3*x3^8 + 159*x1*x2^3*x3^7 + 188*x1*x2^3*x3^6 + 215*x1*x2^3*x3^5 + 268*x1*x2^3*x3^4 + 209*x1*x2^3*x3^3 + 183*x1*x2^3*x3^2 + 127*x1*x2^3*x3 + 85*x1*x2^3 + 17*x1*x2^2*x3^10 + 70*x1*x2^2*x3^9 + 86*x1*x2^2*x3^8 + 120*x1*x2^2*x3^7 + 124*x1*x2^2*x3^6 + 174*x1*x2^2*x3^5 + 191*x1*x2^2*x3^4 + 183*x1*x2^2*x3^3 + 169*x1*x2^2*x3^2 + 137*x1*x2^2*x3 + 55*x1*x2^2 + 11*x1*x2*x3^10 + 25*x1*x2*x3^9 + 62*x1*x2*x3^8 + 40*x1*x2*x3^7 + 80*x1*x2*x3^6 + 122*x1*x2*x3^5 + 122*x1*x2*x3^4 + 127*x1*x2*x3^3 + 137*x1*x2*x3^2 + 117*x1*x2*x3 + 13*x1*x2 + 6*x1*x3^10 + 25*x1*x3^9 + 20*x1*x3^8 + 37*x1*x3^7 + 55*x1*x3^6 + 77*x1*x3^5 + 67*x1*x3^4 + 85*x1*x3^3 + 55*x1*x3^2 + 13*x1*x3 + 3*x1 + 21*x2^10*x3^10 + 6*x2^10*x3^9 + 11*x2^10*x3^8 + 17*x2^10*x3^7 + 34*x2^10*x3^6 + 27*x2^10*x3^5 + 34*x2^10*x3^4 + 17*x2^10*x3^3 + 11*x2^10*x3^2 + 6*x2^10*x3 + 21*x2^10 + 6*x2^9*x3^10 + 24*x2^9*x3^9 + 21*x2^9*x3^8 + 47*x2^9*x3^7 + 75*x2^9*x3^6 + 67*x2^9*x3^5 + 50*x2^9*x3^4 + 59*x2^9*x3^3 + 19*x2^9*x3^2 + 25*x2^9*x3 + 13*x2^9 + 11*x2^8*x3^10 + 21*x2^8*x3^9 + 84*x2^8*x3^8 + 82*x2^8*x3^7 + 100*x2^8*x3^6 + 98*x2^8*x3^5 + 85*x2^8*x3^4 + 67*x2^8*x3^3 + 58*x2^8*x3^2 + 20*x2^8*x3 + 37*x2^8 + 17*x2^7*x3^10 + 47*x2^7*x3^9 + 82*x2^7*x3^8 + 139*x2^7*x3^7 + 98*x2^7*x3^6 + 98*x2^7*x3^5 + 92*x2^7*x3^4 + 83*x2^7*x3^3 + 33*x2^7*x3^2 + 37*x2^7*x3 + 39*x2^7 + 34*x2^6*x3^10 + 75*x2^6*x3^9 + 100*x2^6*x3^8 + 98*x2^6*x3^7 + 155*x2^6*x3^6 + 108*x2^6*x3^5 + 126*x2^6*x3^4 + 104*x2^6*x3^3 + 80*x2^6*x3^2 + 55*x2^6*x3 + 57*x2^6 + 27*x2^5*x3^10 + 67*x2^5*x3^9 + 98*x2^5*x3^8 + 98*x2^5*x3^7 + 108*x2^5*x3^6 + 175*x2^5*x3^5 + 124*x2^5*x3^4 + 131*x2^5*x3^3 + 106*x2^5*x3^2 + 77*x2^5*x3 + 49*x2^5 + 34*x2^4*x3^10 + 50*x2^4*x3^9 + 85*x2^4*x3^8 + 92*x2^4*x3^7 + 126*x2^4*x3^6 + 124*x2^4*x3^5 + 174*x2^4*x3^4 + 124*x2^4*x3^3 + 102*x2^4*x3^2 + 67*x2^4*x3 + 43*x2^4 + 17*x2^3*x3^10 + 59*x2^3*x3^9 + 67*x2^3*x3^8 + 83*x2^3*x3^7 + 104*x2^3*x3^6 + 131*x2^3*x3^5 + 124*x2^3*x3^4 + 138*x2^3*x3^3 + 109*x2^3*x3^2 + 85*x2^3*x3 + 36*x2^3 + 11*x2^2*x3^10 + 19*x2^2*x3^9 + 58*x2^2*x3^8 + 33*x2^2*x3^7 + 80*x2^2*x3^6 + 106*x2^2*x3^5 + 102*x2^2*x3^4 + 109*x2^2*x3^3 + 95*x2^2*x3^2 + 55*x2^2*x3 + 10*x2^2 + 6*x2*x3^10 + 25*x2*x3^9 + 20*x2*x3^8 + 37*x2*x3^7 + 55*x2*x3^6 + 77*x2*x3^5 + 67*x2*x3^4 + 85*x2*x3^3 + 55*x2*x3^2 + 13*x2*x3 + 3*x2 + 21*x3^10 + 13*x3^9 + 37*x3^8 + 39*x3^7 + 57*x3^6 + 49*x3^5 + 43*x3^4 + 36*x3^3 + 10*x3^2 + 3*x3

==================
dimension is P(1, 1, 1) = 128624
==================
Pz = P(z ^ v[1], z ^ v[2], z ^ v[3]) = 21*z^80 + 6*z^79 + 11*z^78 + 17*z^77 + 34*z^76 + 27*z^75 + 34*z^74 + 23*z^73 + 35*z^72 + 48*z^71 + 74*z^70 + 86*z^69 + 84*z^68 + 84*z^67 + 97*z^66 + 95*z^65 + 138*z^64 + 141*z^63 + 165*z^62 + 185*z^61 + 198*z^60 + 202*z^59 + 212*z^58 + 234*z^57 + 298*z^56 + 283*z^55 + 301*z^54 + 318*z^53 + 352*z^52 + 376*z^51 + 400*z^50 + 443*z^49 + 482*z^48 + 480*z^47 + 516*z^46 + 533*z^45 + 583*z^44 + 612*z^43 + 655*z^42 + 668*z^41 + 720*z^40 + 748*z^39 + 785*z^38 + 801*z^37 + 860*z^36 + 879*z^35 + 926*z^34 + 952*z^33 + 1011*z^32 + 1023*z^31 + 1080*z^30 + 1107*z^29 + 1144*z^28 + 1168*z^27 + 1216*z^26 + 1240*z^25 + 1293*z^24 + 1319*z^23 + 1375*z^22 + 1374*z^21 + 1421*z^20 + 1434*z^19 + 1473*z^18 + 1506*z^17 + 1562*z^16 + 1572*z^15 + 1593*z^14 + 1609*z^13 + 1629*z^12 + 1639*z^11 + 1702*z^10 + 1683*z^9 + 1744*z^8 + 1744*z^7 + 1745*z^6 + 1743*z^5 + 1748*z^4 + 1746*z^3 + 1768*z^2 + 1772*z + 1814 + 1772*z^-1 + 1768*z^-2 + 1746*z^-3 + 1748*z^-4 + 1743*z^-5 + 1745*z^-6 + 1744*z^-7 + 1744*z^-8 + 1683*z^-9 + 1702*z^-10 + 1639*z^-11 + 1629*z^-12 + 1609*z^-13 + 1593*z^-14 + 1572*z^-15 + 1562*z^-16 + 1506*z^-17 + 1473*z^-18 + 1434*z^-19 + 1421*z^-20 + 1374*z^-21 + 1375*z^-22 + 1319*z^-23 + 1293*z^-24 + 1240*z^-25 + 1216*z^-26 + 1168*z^-27 + 1144*z^-28 + 1107*z^-29 + 1080*z^-30 + 1023*z^-31 + 1011*z^-32 + 952*z^-33 + 926*z^-34 + 879*z^-35 + 860*z^-36 + 801*z^-37 + 785*z^-38 + 748*z^-39 + 720*z^-40 + 668*z^-41 + 655*z^-42 + 612*z^-43 + 583*z^-44 + 533*z^-45 + 516*z^-46 + 480*z^-47 + 482*z^-48 + 443*z^-49 + 400*z^-50 + 376*z^-51 + 352*z^-52 + 318*z^-53 + 301*z^-54 + 283*z^-55 + 298*z^-56 + 234*z^-57 + 212*z^-58 + 202*z^-59 + 198*z^-60 + 185*z^-61 + 165*z^-62 + 141*z^-63 + 138*z^-64 + 95*z^-65 + 97*z^-66 + 84*z^-67 + 84*z^-68 + 86*z^-69 + 74*z^-70 + 48*z^-71 + 35*z^-72 + 23*z^-73 + 34*z^-74 + 27*z^-75 + 34*z^-76 + 17*z^-77 + 11*z^-78 + 6*z^-79 + 21*z^-80

Using SCIP to solve the ILP requires a few steps: 1. Save ILP as .lp file 2. Open SCIP, read file, solve ILP, and write solution to file 3. Read solution file into Julia and verify

We give an example below.

v = [1,1,-2];
w = [1,4,-5];
k = 106;
m = lp(k,v,w;integer=true);

save_lp("11_14.lp",m)

In SCIP

> read 11_14.lp
> optimize
> set write printzeros TRUE
> write solution 11_14.sol

In Julia

sol = extract_vector("11_14.sol");
@show sol;

sol = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 13, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 3, 0, 0, 0, 0, 0, 3, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 7, 7, 0, 0, 8, 59, 0, 0, 0, 0, 115, 0, 0, 8, 0, 0, 4, 7, 0, 0, 7, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

Finally, we verify that this numerical solution is indeed correct and display the solution in a nice way.

verify_solution(sol,k,v,w);

dimension P(1, 1, 1) = 3216
Pv == Qw = true
check 3rd root of unity P(xi, xi, xi) == P(1, 1, 1) = false
Q(xi, xi, xi) == Q(1, 1, 1) = false

display_solution(sol,k,v,w);

In the Schur basis, P = 4s_{4, 4} + 13s_{5} + 4s_{6, 5} + 3s_{7, 1} + 3s_{7, 7} + 3s_{8} + 4s_{10, 10} + s_{13, 7} + 7s_{13, 13} + 7s_{14}
==================
In the Schur basis, Q = 8s_{1, 1} + 59s_{2} + 115s_{3, 2} + 8s_{4, 1} + 4s_{4, 4} + 7s_{5} + 7s_{5, 3} + 7s_{6, 2}
==================
P = dot_prod(sol_v, list_s) = 7*x1^14 + 7*x1^13*x2^13 + 7*x1^13*x2^12*x3 + 7*x1^13*x2^11*x3^2 + 7*x1^13*x2^10*x3^3 + 7*x1^13*x2^9*x3^4 + 7*x1^13*x2^8*x3^5 + 7*x1^13*x2^7*x3^6 + x1^13*x2^7 + 7*x1^13*x2^6*x3^7 + x1^13*x2^6*x3 + 7*x1^13*x2^5*x3^8 + x1^13*x2^5*x3^2 + 7*x1^13*x2^4*x3^9 + x1^13*x2^4*x3^3 + 7*x1^13*x2^3*x3^10 + x1^13*x2^3*x3^4 + 7*x1^13*x2^2*x3^11 + x1^13*x2^2*x3^5 + 7*x1^13*x2*x3^12 + x1^13*x2*x3^6 + 7*x1^13*x2 + 7*x1^13*x3^13 + x1^13*x3^7 + 7*x1^13*x3 + 7*x1^12*x2^13*x3 + 7*x1^12*x2^12*x3^2 + 7*x1^12*x2^11*x3^3 + 7*x1^12*x2^10*x3^4 + 7*x1^12*x2^9*x3^5 + 7*x1^12*x2^8*x3^6 + x1^12*x2^8 + 7*x1^12*x2^7*x3^7 + 2*x1^12*x2^7*x3 + 7*x1^12*x2^6*x3^8 + 2*x1^12*x2^6*x3^2 + 7*x1^12*x2^5*x3^9 + 2*x1^12*x2^5*x3^3 + 7*x1^12*x2^4*x3^10 + 2*x1^12*x2^4*x3^4 + 7*x1^12*x2^3*x3^11 + 2*x1^12*x2^3*x3^5 + 7*x1^12*x2^2*x3^12 + 2*x1^12*x2^2*x3^6 + 7*x1^12*x2^2 + 7*x1^12*x2*x3^13 + 2*x1^12*x2*x3^7 + 7*x1^12*x2*x3 + x1^12*x3^8 + 7*x1^12*x3^2 + 7*x1^11*x2^13*x3^2 + 7*x1^11*x2^12*x3^3 + 7*x1^11*x2^11*x3^4 + 7*x1^11*x2^10*x3^5 + 7*x1^11*x2^9*x3^6 + x1^11*x2^9 + 7*x1^11*x2^8*x3^7 + 2*x1^11*x2^8*x3 + 7*x1^11*x2^7*x3^8 + 3*x1^11*x2^7*x3^2 + 7*x1^11*x2^6*x3^9 + 3*x1^11*x2^6*x3^3 + 7*x1^11*x2^5*x3^10 + 3*x1^11*x2^5*x3^4 + 7*x1^11*x2^4*x3^11 + 3*x1^11*x2^4*x3^5 + 7*x1^11*x2^3*x3^12 + 3*x1^11*x2^3*x3^6 + 7*x1^11*x2^3 + 7*x1^11*x2^2*x3^13 + 3*x1^11*x2^2*x3^7 + 7*x1^11*x2^2*x3 + 2*x1^11*x2*x3^8 + 7*x1^11*x2*x3^2 + x1^11*x3^9 + 7*x1^11*x3^3 + 7*x1^10*x2^13*x3^3 + 7*x1^10*x2^12*x3^4 + 7*x1^10*x2^11*x3^5 + 7*x1^10*x2^10*x3^6 + 5*x1^10*x2^10 + 7*x1^10*x2^9*x3^7 + 6*x1^10*x2^9*x3 + 7*x1^10*x2^8*x3^8 + 7*x1^10*x2^8*x3^2 + 7*x1^10*x2^7*x3^9 + 8*x1^10*x2^7*x3^3 + 7*x1^10*x2^6*x3^10 + 8*x1^10*x2^6*x3^4 + 7*x1^10*x2^5*x3^11 + 8*x1^10*x2^5*x3^5 + 7*x1^10*x2^4*x3^12 + 8*x1^10*x2^4*x3^6 + 7*x1^10*x2^4 + 7*x1^10*x2^3*x3^13 + 8*x1^10*x2^3*x3^7 + 7*x1^10*x2^3*x3 + 7*x1^10*x2^2*x3^8 + 7*x1^10*x2^2*x3^2 + 6*x1^10*x2*x3^9 + 7*x1^10*x2*x3^3 + 5*x1^10*x3^10 + 7*x1^10*x3^4 + 7*x1^9*x2^13*x3^4 + 7*x1^9*x2^12*x3^5 + 7*x1^9*x2^11*x3^6 + x1^9*x2^11 + 7*x1^9*x2^10*x3^7 + 6*x1^9*x2^10*x3 + 7*x1^9*x2^9*x3^8 + 7*x1^9*x2^9*x3^2 + 7*x1^9*x2^8*x3^9 + 8*x1^9*x2^8*x3^3 + 7*x1^9*x2^7*x3^10 + 9*x1^9*x2^7*x3^4 + 7*x1^9*x2^6*x3^11 + 9*x1^9*x2^6*x3^5 + 7*x1^9*x2^5*x3^12 + 9*x1^9*x2^5*x3^6 + 7*x1^9*x2^5 + 7*x1^9*x2^4*x3^13 + 9*x1^9*x2^4*x3^7 + 7*x1^9*x2^4*x3 + 8*x1^9*x2^3*x3^8 + 7*x1^9*x2^3*x3^2 + 7*x1^9*x2^2*x3^9 + 7*x1^9*x2^2*x3^3 + 6*x1^9*x2*x3^10 + 7*x1^9*x2*x3^4 + x1^9*x3^11 + 7*x1^9*x3^5 + 7*x1^8*x2^13*x3^5 + 7*x1^8*x2^12*x3^6 + x1^8*x2^12 + 7*x1^8*x2^11*x3^7 + 2*x1^8*x2^11*x3 + 7*x1^8*x2^10*x3^8 + 7*x1^8*x2^10*x3^2 + 7*x1^8*x2^9*x3^9 + 8*x1^8*x2^9*x3^3 + 7*x1^8*x2^8*x3^10 + 9*x1^8*x2^8*x3^4 + 7*x1^8*x2^7*x3^11 + 10*x1^8*x2^7*x3^5 + 7*x1^8*x2^6*x3^12 + 10*x1^8*x2^6*x3^6 + 7*x1^8*x2^6 + 7*x1^8*x2^5*x3^13 + 10*x1^8*x2^5*x3^7 + 7*x1^8*x2^5*x3 + 9*x1^8*x2^4*x3^8 + 7*x1^8*x2^4*x3^2 + 8*x1^8*x2^3*x3^9 + 7*x1^8*x2^3*x3^3 + 7*x1^8*x2^2*x3^10 + 7*x1^8*x2^2*x3^4 + 2*x1^8*x2*x3^11 + 7*x1^8*x2*x3^5 + x1^8*x3^12 + 7*x1^8*x3^6 + 3*x1^8 + 7*x1^7*x2^13*x3^6 + x1^7*x2^13 + 7*x1^7*x2^12*x3^7 + 2*x1^7*x2^12*x3 + 7*x1^7*x2^11*x3^8 + 3*x1^7*x2^11*x3^2 + 7*x1^7*x2^10*x3^9 + 8*x1^7*x2^10*x3^3 + 7*x1^7*x2^9*x3^10 + 9*x1^7*x2^9*x3^4 + 7*x1^7*x2^8*x3^11 + 10*x1^7*x2^8*x3^5 + 7*x1^7*x2^7*x3^12 + 11*x1^7*x2^7*x3^6 + 10*x1^7*x2^7 + 7*x1^7*x2^6*x3^13 + 11*x1^7*x2^6*x3^7 + 10*x1^7*x2^6*x3 + 10*x1^7*x2^5*x3^8 + 10*x1^7*x2^5*x3^2 + 9*x1^7*x2^4*x3^9 + 10*x1^7*x2^4*x3^3 + 8*x1^7*x2^3*x3^10 + 10*x1^7*x2^3*x3^4 + 3*x1^7*x2^2*x3^11 + 10*x1^7*x2^2*x3^5 + 2*x1^7*x2*x3^12 + 10*x1^7*x2*x3^6 + 6*x1^7*x2 + x1^7*x3^13 + 10*x1^7*x3^7 + 6*x1^7*x3 + 7*x1^6*x2^13*x3^7 + x1^6*x2^13*x3 + 7*x1^6*x2^12*x3^8 + 2*x1^6*x2^12*x3^2 + 7*x1^6*x2^11*x3^9 + 3*x1^6*x2^11*x3^3 + 7*x1^6*x2^10*x3^10 + 8*x1^6*x2^10*x3^4 + 7*x1^6*x2^9*x3^11 + 9*x1^6*x2^9*x3^5 + 7*x1^6*x2^8*x3^12 + 10*x1^6*x2^8*x3^6 + 7*x1^6*x2^8 + 7*x1^6*x2^7*x3^13 + 11*x1^6*x2^7*x3^7 + 10*x1^6*x2^7*x3 + 10*x1^6*x2^6*x3^8 + 10*x1^6*x2^6*x3^2 + 9*x1^6*x2^5*x3^9 + 10*x1^6*x2^5*x3^3 + 4*x1^6*x2^5 + 8*x1^6*x2^4*x3^10 + 10*x1^6*x2^4*x3^4 + 4*x1^6*x2^4*x3 + 3*x1^6*x2^3*x3^11 + 10*x1^6*x2^3*x3^5 + 4*x1^6*x2^3*x3^2 + 2*x1^6*x2^2*x3^12 + 10*x1^6*x2^2*x3^6 + 4*x1^6*x2^2*x3^3 + 6*x1^6*x2^2 + x1^6*x2*x3^13 + 10*x1^6*x2*x3^7 + 4*x1^6*x2*x3^4 + 9*x1^6*x2*x3 + 7*x1^6*x3^8 + 4*x1^6*x3^5 + 6*x1^6*x3^2 + 7*x1^5*x2^13*x3^8 + x1^5*x2^13*x3^2 + 7*x1^5*x2^12*x3^9 + 2*x1^5*x2^12*x3^3 + 7*x1^5*x2^11*x3^10 + 3*x1^5*x2^11*x3^4 + 7*x1^5*x2^10*x3^11 + 8*x1^5*x2^10*x3^5 + 7*x1^5*x2^9*x3^12 + 9*x1^5*x2^9*x3^6 + 7*x1^5*x2^9 + 7*x1^5*x2^8*x3^13 + 10*x1^5*x2^8*x3^7 + 7*x1^5*x2^8*x3 + 10*x1^5*x2^7*x3^8 + 10*x1^5*x2^7*x3^2 + 9*x1^5*x2^6*x3^9 + 10*x1^5*x2^6*x3^3 + 4*x1^5*x2^6 + 8*x1^5*x2^5*x3^10 + 10*x1^5*x2^5*x3^4 + 8*x1^5*x2^5*x3 + 3*x1^5*x2^4*x3^11 + 10*x1^5*x2^4*x3^5 + 8*x1^5*x2^4*x3^2 + 2*x1^5*x2^3*x3^12 + 10*x1^5*x2^3*x3^6 + 8*x1^5*x2^3*x3^3 + 6*x1^5*x2^3 + x1^5*x2^2*x3^13 + 10*x1^5*x2^2*x3^7 + 8*x1^5*x2^2*x3^4 + 9*x1^5*x2^2*x3 + 7*x1^5*x2*x3^8 + 8*x1^5*x2*x3^5 + 9*x1^5*x2*x3^2 + 7*x1^5*x3^9 + 4*x1^5*x3^6 + 6*x1^5*x3^3 + 13*x1^5 + 7*x1^4*x2^13*x3^9 + x1^4*x2^13*x3^3 + 7*x1^4*x2^12*x3^10 + 2*x1^4*x2^12*x3^4 + 7*x1^4*x2^11*x3^11 + 3*x1^4*x2^11*x3^5 + 7*x1^4*x2^10*x3^12 + 8*x1^4*x2^10*x3^6 + 7*x1^4*x2^10 + 7*x1^4*x2^9*x3^13 + 9*x1^4*x2^9*x3^7 + 7*x1^4*x2^9*x3 + 9*x1^4*x2^8*x3^8 + 7*x1^4*x2^8*x3^2 + 9*x1^4*x2^7*x3^9 + 10*x1^4*x2^7*x3^3 + 8*x1^4*x2^6*x3^10 + 10*x1^4*x2^6*x3^4 + 4*x1^4*x2^6*x3 + 3*x1^4*x2^5*x3^11 + 10*x1^4*x2^5*x3^5 + 8*x1^4*x2^5*x3^2 + 2*x1^4*x2^4*x3^12 + 10*x1^4*x2^4*x3^6 + 8*x1^4*x2^4*x3^3 + 10*x1^4*x2^4 + x1^4*x2^3*x3^13 + 10*x1^4*x2^3*x3^7 + 8*x1^4*x2^3*x3^4 + 13*x1^4*x2^3*x3 + 7*x1^4*x2^2*x3^8 + 8*x1^4*x2^2*x3^5 + 13*x1^4*x2^2*x3^2 + 7*x1^4*x2*x3^9 + 4*x1^4*x2*x3^6 + 13*x1^4*x2*x3^3 + 13*x1^4*x2 + 7*x1^4*x3^10 + 10*x1^4*x3^4 + 13*x1^4*x3 + 7*x1^3*x2^13*x3^10 + x1^3*x2^13*x3^4 + 7*x1^3*x2^12*x3^11 + 2*x1^3*x2^12*x3^5 + 7*x1^3*x2^11*x3^12 + 3*x1^3*x2^11*x3^6 + 7*x1^3*x2^11 + 7*x1^3*x2^10*x3^13 + 8*x1^3*x2^10*x3^7 + 7*x1^3*x2^10*x3 + 8*x1^3*x2^9*x3^8 + 7*x1^3*x2^9*x3^2 + 8*x1^3*x2^8*x3^9 + 7*x1^3*x2^8*x3^3 + 8*x1^3*x2^7*x3^10 + 10*x1^3*x2^7*x3^4 + 3*x1^3*x2^6*x3^11 + 10*x1^3*x2^6*x3^5 + 4*x1^3*x2^6*x3^2 + 2*x1^3*x2^5*x3^12 + 10*x1^3*x2^5*x3^6 + 8*x1^3*x2^5*x3^3 + 6*x1^3*x2^5 + x1^3*x2^4*x3^13 + 10*x1^3*x2^4*x3^7 + 8*x1^3*x2^4*x3^4 + 13*x1^3*x2^4*x3 + 7*x1^3*x2^3*x3^8 + 8*x1^3*x2^3*x3^5 + 13*x1^3*x2^3*x3^2 + 7*x1^3*x2^2*x3^9 + 4*x1^3*x2^2*x3^6 + 13*x1^3*x2^2*x3^3 + 13*x1^3*x2^2 + 7*x1^3*x2*x3^10 + 13*x1^3*x2*x3^4 + 13*x1^3*x2*x3 + 7*x1^3*x3^11 + 6*x1^3*x3^5 + 13*x1^3*x3^2 + 7*x1^2*x2^13*x3^11 + x1^2*x2^13*x3^5 + 7*x1^2*x2^12*x3^12 + 2*x1^2*x2^12*x3^6 + 7*x1^2*x2^12 + 7*x1^2*x2^11*x3^13 + 3*x1^2*x2^11*x3^7 + 7*x1^2*x2^11*x3 + 7*x1^2*x2^10*x3^8 + 7*x1^2*x2^10*x3^2 + 7*x1^2*x2^9*x3^9 + 7*x1^2*x2^9*x3^3 + 7*x1^2*x2^8*x3^10 + 7*x1^2*x2^8*x3^4 + 3*x1^2*x2^7*x3^11 + 10*x1^2*x2^7*x3^5 + 2*x1^2*x2^6*x3^12 + 10*x1^2*x2^6*x3^6 + 4*x1^2*x2^6*x3^3 + 6*x1^2*x2^6 + x1^2*x2^5*x3^13 + 10*x1^2*x2^5*x3^7 + 8*x1^2*x2^5*x3^4 + 9*x1^2*x2^5*x3 + 7*x1^2*x2^4*x3^8 + 8*x1^2*x2^4*x3^5 + 13*x1^2*x2^4*x3^2 + 7*x1^2*x2^3*x3^9 + 4*x1^2*x2^3*x3^6 + 13*x1^2*x2^3*x3^3 + 13*x1^2*x2^3 + 7*x1^2*x2^2*x3^10 + 13*x1^2*x2^2*x3^4 + 13*x1^2*x2^2*x3 + 7*x1^2*x2*x3^11 + 9*x1^2*x2*x3^5 + 13*x1^2*x2*x3^2 + 7*x1^2*x3^12 + 6*x1^2*x3^6 + 13*x1^2*x3^3 + 7*x1*x2^13*x3^12 + x1*x2^13*x3^6 + 7*x1*x2^13 + 7*x1*x2^12*x3^13 + 2*x1*x2^12*x3^7 + 7*x1*x2^12*x3 + 2*x1*x2^11*x3^8 + 7*x1*x2^11*x3^2 + 6*x1*x2^10*x3^9 + 7*x1*x2^10*x3^3 + 6*x1*x2^9*x3^10 + 7*x1*x2^9*x3^4 + 2*x1*x2^8*x3^11 + 7*x1*x2^8*x3^5 + 2*x1*x2^7*x3^12 + 10*x1*x2^7*x3^6 + 6*x1*x2^7 + x1*x2^6*x3^13 + 10*x1*x2^6*x3^7 + 4*x1*x2^6*x3^4 + 9*x1*x2^6*x3 + 7*x1*x2^5*x3^8 + 8*x1*x2^5*x3^5 + 9*x1*x2^5*x3^2 + 7*x1*x2^4*x3^9 + 4*x1*x2^4*x3^6 + 13*x1*x2^4*x3^3 + 13*x1*x2^4 + 7*x1*x2^3*x3^10 + 13*x1*x2^3*x3^4 + 13*x1*x2^3*x3 + 7*x1*x2^2*x3^11 + 9*x1*x2^2*x3^5 + 13*x1*x2^2*x3^2 + 7*x1*x2*x3^12 + 9*x1*x2*x3^6 + 13*x1*x2*x3^3 + 7*x1*x3^13 + 6*x1*x3^7 + 13*x1*x3^4 + 7*x2^14 + 7*x2^13*x3^13 + x2^13*x3^7 + 7*x2^13*x3 + x2^12*x3^8 + 7*x2^12*x3^2 + x2^11*x3^9 + 7*x2^11*x3^3 + 5*x2^10*x3^10 + 7*x2^10*x3^4 + x2^9*x3^11 + 7*x2^9*x3^5 + x2^8*x3^12 + 7*x2^8*x3^6 + 3*x2^8 + x2^7*x3^13 + 10*x2^7*x3^7 + 6*x2^7*x3 + 7*x2^6*x3^8 + 4*x2^6*x3^5 + 6*x2^6*x3^2 + 7*x2^5*x3^9 + 4*x2^5*x3^6 + 6*x2^5*x3^3 + 13*x2^5 + 7*x2^4*x3^10 + 10*x2^4*x3^4 + 13*x2^4*x3 + 7*x2^3*x3^11 + 6*x2^3*x3^5 + 13*x2^3*x3^2 + 7*x2^2*x3^12 + 6*x2^2*x3^6 + 13*x2^2*x3^3 + 7*x2*x3^13 + 6*x2*x3^7 + 13*x2*x3^4 + 7*x3^14 + 3*x3^8 + 13*x3^5
==================
Q = dot_prod(sol_w, list_s) = 7*x1^6*x2^2 + 7*x1^6*x2*x3 + 7*x1^6*x3^2 + 14*x1^5*x2^3 + 21*x1^5*x2^2*x3 + 21*x1^5*x2*x3^2 + 14*x1^5*x3^3 + 7*x1^5 + 18*x1^4*x2^4 + 32*x1^4*x2^3*x3 + 39*x1^4*x2^2*x3^2 + 32*x1^4*x2*x3^3 + 15*x1^4*x2 + 18*x1^4*x3^4 + 15*x1^4*x3 + 14*x1^3*x2^5 + 32*x1^3*x2^4*x3 + 46*x1^3*x2^3*x3^2 + 46*x1^3*x2^2*x3^3 + 130*x1^3*x2^2 + 32*x1^3*x2*x3^4 + 138*x1^3*x2*x3 + 14*x1^3*x3^5 + 130*x1^3*x3^2 + 7*x1^2*x2^6 + 21*x1^2*x2^5*x3 + 39*x1^2*x2^4*x3^2 + 46*x1^2*x2^3*x3^3 + 130*x1^2*x2^3 + 39*x1^2*x2^2*x3^4 + 253*x1^2*x2^2*x3 + 21*x1^2*x2*x3^5 + 253*x1^2*x2*x3^2 + 7*x1^2*x3^6 + 130*x1^2*x3^3 + 59*x1^2 + 7*x1*x2^6*x3 + 21*x1*x2^5*x3^2 + 32*x1*x2^4*x3^3 + 15*x1*x2^4 + 32*x1*x2^3*x3^4 + 138*x1*x2^3*x3 + 21*x1*x2^2*x3^5 + 253*x1*x2^2*x3^2 + 7*x1*x2*x3^6 + 138*x1*x2*x3^3 + 67*x1*x2 + 15*x1*x3^4 + 67*x1*x3 + 7*x2^6*x3^2 + 14*x2^5*x3^3 + 7*x2^5 + 18*x2^4*x3^4 + 15*x2^4*x3 + 14*x2^3*x3^5 + 130*x2^3*x3^2 + 7*x2^2*x3^6 + 130*x2^2*x3^3 + 59*x2^2 + 15*x2*x3^4 + 67*x2*x3 + 7*x3^5 + 59*x3^2
==================
dimension is P(1, 1, 1) = 3216
==================
Pz = P(z ^ v[1], z ^ v[2], z ^ v[3]) = 7*z^26 + 14*z^23 + 32*z^20 + 50*z^17 + 176*z^14 + 198*z^11 + 272*z^8 + 394*z^5 + 398*z^2 + 402*z^-1 + 391*z^-4 + 324*z^-7 + 250*z^-10 + 176*z^-13 + 54*z^-16 + 36*z^-19 + 21*z^-22 + 14*z^-25 + 7*z^-28