#vars [ x1, x2, x3, x4, x5, x6, x7, x8 ] #modulo 65521 #list [ 99*x1^3 + 24067*x1^2*x2 + 41652*x1*x2^2 + 99*x2^3 + 189*x1^2*x3 + 186*x1*x2*x3 + 24067*x2^2*x3 + 189*x1*x3^2 + 41652*x2*x3^2 + 99*x3^3 + 41652*x1^2*x4 + 186*x1*x2*x4 + 189*x2^2*x4 + 186*x1*x3*x4 + 186*x2*x3*x4 + 24067*x3^2*x4 + 24067*x1*x4^2 + 189*x2*x4^2 + 41652*x3*x4^2 + 99*x4^3 + 65421*x1^2*x5 + 18*x1*x2*x5 + 65421*x2^2*x5 + 65493*x1*x3*x5 + 18*x2*x3*x5 + 65421*x3^2*x5 + 18*x1*x4*x5 + 65493*x2*x4*x5 + 18*x3*x4*x5 + 65421*x4^2*x5 + 21*x1*x5^2 + 21*x2*x5^2 + 21*x3*x5^2 + 21*x4*x5^2 + 65384*x5^3 + 65421*x1^2*x6 + 18*x1*x2*x6 + 65421*x2^2*x6 + 65493*x1*x3*x6 + 18*x2*x3*x6 + 65421*x3^2*x6 + 18*x1*x4*x6 + 65493*x2*x4*x6 + 18*x3*x4*x6 + 65421*x4^2*x6 + 32*x1*x5*x6 + 32*x2*x5*x6 + 32*x3*x5*x6 + 32*x4*x5*x6 + 65516*x5^2*x6 + 21*x1*x6^2 + 21*x2*x6^2 + 21*x3*x6^2 + 21*x4*x6^2 + 65516*x5*x6^2 + 65384*x6^3 + 65421*x1^2*x7 + 18*x1*x2*x7 + 65421*x2^2*x7 + 65493*x1*x3*x7 + 18*x2*x3*x7 + 65421*x3^2*x7 + 18*x1*x4*x7 + 65493*x2*x4*x7 + 18*x3*x4*x7 + 65421*x4^2*x7 + 38*x1*x5*x7 + 38*x2*x5*x7 + 38*x3*x5*x7 + 38*x4*x5*x7 + 65434*x5^2*x7 + 32*x1*x6*x7 + 32*x2*x6*x7 + 32*x3*x6*x7 + 32*x4*x6*x7 + 65227*x5*x6*x7 + 65516*x6^2*x7 + 21*x1*x7^2 + 21*x2*x7^2 + 21*x3*x7^2 + 21*x4*x7^2 + 65434*x5*x7^2 + 65516*x6*x7^2 + 65384*x7^3 + 65421*x1^2*x8 + 18*x1*x2*x8 + 65421*x2^2*x8 + 65493*x1*x3*x8 + 18*x2*x3*x8 + 65421*x3^2*x8 + 18*x1*x4*x8 + 65493*x2*x4*x8 + 18*x3*x4*x8 + 65421*x4^2*x8 + 32*x1*x5*x8 + 32*x2*x5*x8 + 32*x3*x5*x8 + 32*x4*x5*x8 + 65516*x5^2*x8 + 38*x1*x6*x8 + 38*x2*x6*x8 + 38*x3*x6*x8 + 38*x4*x6*x8 + 65227*x5*x6*x8 + 65434*x6^2*x8 + 32*x1*x7*x8 + 32*x2*x7*x8 + 32*x3*x7*x8 + 32*x4*x7*x8 + 65227*x5*x7*x8 + 65227*x6*x7*x8 + 65516*x7^2*x8 + 21*x1*x8^2 + 21*x2*x8^2 + 21*x3*x8^2 + 21*x4*x8^2 + 65516*x5*x8^2 + 65434*x6*x8^2 + 65516*x7*x8^2 + 65384*x8^3 + 65499*x1^2 + 20*x1*x2 + 65499*x2^2 + 65413*x1*x3 + 20*x2*x3 + 65499*x3^2 + 20*x1*x4 + 65413*x2*x4 + 20*x3*x4 + 65499*x4^2 + 36*x1*x5 + 36*x2*x5 + 36*x3*x5 + 36*x4*x5 + 8*x5^2 + 36*x1*x6 + 36*x2*x6 + 36*x3*x6 + 36*x4*x6 + 6*x5*x6 + 8*x6^2 + 36*x1*x7 + 36*x2*x7 + 36*x3*x7 + 36*x4*x7 + 156*x5*x7 + 6*x6*x7 + 8*x7^2 + 36*x1*x8 + 36*x2*x8 + 36*x3*x8 + 36*x4*x8 + 6*x5*x8 + 156*x6*x8 + 6*x7*x8 + 8*x8^2 + 65503*x1 + 65503*x2 + 65503*x3 + 65503*x4 + 65493*x5 + 65493*x6 + 65493*x7 + 65493*x8 + 37844, 40*x1^3 + 45930*x1^2*x2 + 19775*x1*x2^2 + 40*x2^3 + 32*x1^2*x3 + 224*x1*x2*x3 + 45930*x2^2*x3 + 32*x1*x3^2 + 19775*x2*x3^2 + 40*x3^3 + 19775*x1^2*x4 + 224*x1*x2*x4 + 32*x2^2*x4 + 224*x1*x3*x4 + 224*x2*x3*x4 + 45930*x3^2*x4 + 45930*x1*x4^2 + 32*x2*x4^2 + 19775*x3*x4^2 + 40*x4^3 + 65504*x1^2*x5 + 72*x1*x2*x5 + 65504*x2^2*x5 + 65411*x1*x3*x5 + 72*x2*x3*x5 + 65504*x3^2*x5 + 72*x1*x4*x5 + 65411*x2*x4*x5 + 72*x3*x4*x5 + 65504*x4^2*x5 + 65509*x1*x5^2 + 65509*x2*x5^2 + 65509*x3*x5^2 + 65509*x4*x5^2 + 68*x5^3 + 65504*x1^2*x6 + 72*x1*x2*x6 + 65504*x2^2*x6 + 65411*x1*x3*x6 + 72*x2*x3*x6 + 65504*x3^2*x6 + 72*x1*x4*x6 + 65411*x2*x4*x6 + 72*x3*x4*x6 + 65504*x4^2*x6 + 54*x1*x5*x6 + 54*x2*x5*x6 + 54*x3*x5*x6 + 54*x4*x5*x6 + 56192*x5^2*x6 + 65509*x1*x6^2 + 65509*x2*x6^2 + 65509*x3*x6^2 + 65509*x4*x6^2 + 9305*x5*x6^2 + 68*x6^3 + 65504*x1^2*x7 + 72*x1*x2*x7 + 65504*x2^2*x7 + 65411*x1*x3*x7 + 72*x2*x3*x7 + 65504*x3^2*x7 + 72*x1*x4*x7 + 65411*x2*x4*x7 + 72*x3*x4*x7 + 65504*x4^2*x7 + 20*x1*x5*x7 + 20*x2*x5*x7 + 20*x3*x5*x7 + 20*x4*x5*x7 + 216*x5^2*x7 + 54*x1*x6*x7 + 54*x2*x6*x7 + 54*x3*x6*x7 + 54*x4*x6*x7 + 252*x5*x6*x7 + 56192*x6^2*x7 + 65509*x1*x7^2 + 65509*x2*x7^2 + 65509*x3*x7^2 + 65509*x4*x7^2 + 216*x5*x7^2 + 9305*x6*x7^2 + 68*x7^3 + 65504*x1^2*x8 + 72*x1*x2*x8 + 65504*x2^2*x8 + 65411*x1*x3*x8 + 72*x2*x3*x8 + 65504*x3^2*x8 + 72*x1*x4*x8 + 65411*x2*x4*x8 + 72*x3*x4*x8 + 65504*x4^2*x8 + 54*x1*x5*x8 + 54*x2*x5*x8 + 54*x3*x5*x8 + 54*x4*x5*x8 + 9305*x5^2*x8 + 20*x1*x6*x8 + 20*x2*x6*x8 + 20*x3*x6*x8 + 20*x4*x6*x8 + 252*x5*x6*x8 + 216*x6^2*x8 + 54*x1*x7*x8 + 54*x2*x7*x8 + 54*x3*x7*x8 + 54*x4*x7*x8 + 252*x5*x7*x8 + 252*x6*x7*x8 + 56192*x7^2*x8 + 65509*x1*x8^2 + 65509*x2*x8^2 + 65509*x3*x8^2 + 65509*x4*x8^2 + 56192*x5*x8^2 + 216*x6*x8^2 + 9305*x7*x8^2 + 68*x8^3 + 22*x1^2 + 65421*x1*x2 + 22*x2^2 + 65373*x1*x3 + 65421*x2*x3 + 22*x3^2 + 65421*x1*x4 + 65373*x2*x4 + 65421*x3*x4 + 22*x4^2 + 192*x5*x6 + 16*x5*x7 + 192*x6*x7 + 192*x5*x8 + 16*x6*x8 + 192*x7*x8 + 14*x1 + 14*x2 + 14*x3 + 14*x4 + 65501*x5 + 65501*x6 + 65501*x7 + 65501*x8 + 3211, 15*x1^3 + 8719*x1^2*x2 + 56744*x1*x2^2 + 15*x2^3 + 65282*x1^2*x3 + 65403*x1*x2*x3 + 8719*x2^2*x3 + 65282*x1*x3^2 + 56744*x2*x3^2 + 15*x3^3 + 56744*x1^2*x4 + 65403*x1*x2*x4 + 65282*x2^2*x4 + 65403*x1*x3*x4 + 65403*x2*x3*x4 + 8719*x3^2*x4 + 8719*x1*x4^2 + 65282*x2*x4^2 + 56744*x3*x4^2 + 15*x4^3 + 40*x1^2*x5 + 74*x1*x2*x5 + 40*x2^2*x5 + 60*x1*x3*x5 + 74*x2*x3*x5 + 40*x3^2*x5 + 74*x1*x4*x5 + 60*x2*x4*x5 + 74*x3*x4*x5 + 40*x4^2*x5 + 65461*x1*x5^2 + 65461*x2*x5^2 + 65461*x3*x5^2 + 65461*x4*x5^2 + 65395*x5^3 + 40*x1^2*x6 + 74*x1*x2*x6 + 40*x2^2*x6 + 60*x1*x3*x6 + 74*x2*x3*x6 + 40*x3^2*x6 + 74*x1*x4*x6 + 60*x2*x4*x6 + 74*x3*x4*x6 + 40*x4^2*x6 + 65487*x1*x5*x6 + 65487*x2*x5*x6 + 65487*x3*x5*x6 + 65487*x4*x5*x6 + 22899*x5^2*x6 + 65461*x1*x6^2 + 65461*x2*x6^2 + 65461*x3*x6^2 + 65461*x4*x6^2 + 42582*x5*x6^2 + 65395*x6^3 + 40*x1^2*x7 + 74*x1*x2*x7 + 40*x2^2*x7 + 60*x1*x3*x7 + 74*x2*x3*x7 + 40*x3^2*x7 + 74*x1*x4*x7 + 60*x2*x4*x7 + 74*x3*x4*x7 + 40*x4^2*x7 + 65325*x1*x5*x7 + 65325*x2*x5*x7 + 65325*x3*x5*x7 + 65325*x4*x5*x7 + 65451*x5^2*x7 + 65487*x1*x6*x7 + 65487*x2*x6*x7 + 65487*x3*x6*x7 + 65487*x4*x6*x7 + 44*x5*x6*x7 + 22899*x6^2*x7 + 65461*x1*x7^2 + 65461*x2*x7^2 + 65461*x3*x7^2 + 65461*x4*x7^2 + 65451*x5*x7^2 + 42582*x6*x7^2 + 65395*x7^3 + 40*x1^2*x8 + 74*x1*x2*x8 + 40*x2^2*x8 + 60*x1*x3*x8 + 74*x2*x3*x8 + 40*x3^2*x8 + 74*x1*x4*x8 + 60*x2*x4*x8 + 74*x3*x4*x8 + 40*x4^2*x8 + 65487*x1*x5*x8 + 65487*x2*x5*x8 + 65487*x3*x5*x8 + 65487*x4*x5*x8 + 42582*x5^2*x8 + 65325*x1*x6*x8 + 65325*x2*x6*x8 + 65325*x3*x6*x8 + 65325*x4*x6*x8 + 44*x5*x6*x8 + 65451*x6^2*x8 + 65487*x1*x7*x8 + 65487*x2*x7*x8 + 65487*x3*x7*x8 + 65487*x4*x7*x8 + 44*x5*x7*x8 + 44*x6*x7*x8 + 22899*x7^2*x8 + 65461*x1*x8^2 + 65461*x2*x8^2 + 65461*x3*x8^2 + 65461*x4*x8^2 + 22899*x5*x8^2 + 65451*x6*x8^2 + 42582*x7*x8^2 + 65395*x8^3 + 65509*x1^2 + 65475*x1*x2 + 65509*x2^2 + 65461*x1*x3 + 65475*x2*x3 + 65509*x3^2 + 65475*x1*x4 + 65461*x2*x4 + 65475*x3*x4 + 65509*x4^2 + 22*x1*x5 + 22*x2*x5 + 22*x3*x5 + 22*x4*x5 + 65468*x5^2 + 22*x1*x6 + 22*x2*x6 + 22*x3*x6 + 22*x4*x6 + 65511*x5*x6 + 65468*x6^2 + 22*x1*x7 + 22*x2*x7 + 22*x3*x7 + 22*x4*x7 + 65351*x5*x7 + 65511*x6*x7 + 65468*x7^2 + 22*x1*x8 + 22*x2*x8 + 22*x3*x8 + 22*x4*x8 + 65511*x5*x8 + 65351*x6*x8 + 65511*x7*x8 + 65468*x8^2 + 22*x1 + 22*x2 + 22*x3 + 22*x4 + 65505*x5 + 65505*x6 + 65505*x7 + 65505*x8 + 38261, 48*x1^3 + 65000*x1^2*x2 + 617*x1*x2^2 + 48*x2^3 + 36*x1^2*x3 + 204*x1*x2*x3 + 65000*x2^2*x3 + 36*x1*x3^2 + 617*x2*x3^2 + 48*x3^3 + 617*x1^2*x4 + 204*x1*x2*x4 + 36*x2^2*x4 + 204*x1*x3*x4 + 204*x2*x3*x4 + 65000*x3^2*x4 + 65000*x1*x4^2 + 36*x2*x4^2 + 617*x3*x4^2 + 48*x4^3 + 65415*x1^2*x5 + 68*x1*x2*x5 + 65415*x2^2*x5 + 65477*x1*x3*x5 + 68*x2*x3*x5 + 65415*x3^2*x5 + 68*x1*x4*x5 + 65477*x2*x4*x5 + 68*x3*x4*x5 + 65415*x4^2*x5 + 65510*x1*x5^2 + 65510*x2*x5^2 + 65510*x3*x5^2 + 65510*x4*x5^2 + 87*x5^3 + 65415*x1^2*x6 + 68*x1*x2*x6 + 65415*x2^2*x6 + 65477*x1*x3*x6 + 68*x2*x3*x6 + 65415*x3^2*x6 + 68*x1*x4*x6 + 65477*x2*x4*x6 + 68*x3*x4*x6 + 65415*x4^2*x6 + 65377*x1*x5*x6 + 65377*x2*x5*x6 + 65377*x3*x5*x6 + 65377*x4*x5*x6 + 27308*x5^2*x6 + 65510*x1*x6^2 + 65510*x2*x6^2 + 65510*x3*x6^2 + 65510*x4*x6^2 + 38243*x5*x6^2 + 87*x6^3 + 65415*x1^2*x7 + 68*x1*x2*x7 + 65415*x2^2*x7 + 65477*x1*x3*x7 + 68*x2*x3*x7 + 65415*x3^2*x7 + 68*x1*x4*x7 + 65477*x2*x4*x7 + 68*x3*x4*x7 + 65415*x4^2*x7 + 126*x1*x5*x7 + 126*x2*x5*x7 + 126*x3*x5*x7 + 126*x4*x5*x7 + 201*x5^2*x7 + 65377*x1*x6*x7 + 65377*x2*x6*x7 + 65377*x3*x6*x7 + 65377*x4*x6*x7 + 226*x5*x6*x7 + 27308*x6^2*x7 + 65510*x1*x7^2 + 65510*x2*x7^2 + 65510*x3*x7^2 + 65510*x4*x7^2 + 201*x5*x7^2 + 38243*x6*x7^2 + 87*x7^3 + 65415*x1^2*x8 + 68*x1*x2*x8 + 65415*x2^2*x8 + 65477*x1*x3*x8 + 68*x2*x3*x8 + 65415*x3^2*x8 + 68*x1*x4*x8 + 65477*x2*x4*x8 + 68*x3*x4*x8 + 65415*x4^2*x8 + 65377*x1*x5*x8 + 65377*x2*x5*x8 + 65377*x3*x5*x8 + 65377*x4*x5*x8 + 38243*x5^2*x8 + 126*x1*x6*x8 + 126*x2*x6*x8 + 126*x3*x6*x8 + 126*x4*x6*x8 + 226*x5*x6*x8 + 201*x6^2*x8 + 65377*x1*x7*x8 + 65377*x2*x7*x8 + 65377*x3*x7*x8 + 65377*x4*x7*x8 + 226*x5*x7*x8 + 226*x6*x7*x8 + 27308*x7^2*x8 + 65510*x1*x8^2 + 65510*x2*x8^2 + 65510*x3*x8^2 + 65510*x4*x8^2 + 27308*x5*x8^2 + 201*x6*x8^2 + 38243*x7*x8^2 + 87*x8^3 + 15*x1^2 + 65457*x1*x2 + 15*x2^2 + 34*x1*x3 + 65457*x2*x3 + 15*x3^2 + 65457*x1*x4 + 34*x2*x4 + 65457*x3*x4 + 15*x4^2 + 65472*x1*x5 + 65472*x2*x5 + 65472*x3*x5 + 65472*x4*x5 + 75*x5^2 + 65472*x1*x6 + 65472*x2*x6 + 65472*x3*x6 + 65472*x4*x6 + 44*x5*x6 + 75*x6^2 + 65472*x1*x7 + 65472*x2*x7 + 65472*x3*x7 + 65472*x4*x7 + 50*x5*x7 + 44*x6*x7 + 75*x7^2 + 65472*x1*x8 + 65472*x2*x8 + 65472*x3*x8 + 65472*x4*x8 + 44*x5*x8 + 50*x6*x8 + 44*x7*x8 + 75*x8^2 + 31*x1 + 31*x2 + 31*x3 + 31*x4 + 40*x5 + 40*x6 + 40*x7 + 40*x8 + 15518, 65388*x1^3 + 125*x1^2*x2 + 125*x1*x2^2 + 65388*x2^3 + 33*x1^2*x3 + 202*x1*x2*x3 + 125*x2^2*x3 + 33*x1*x3^2 + 125*x2*x3^2 + 65388*x3^3 + 125*x1^2*x4 + 202*x1*x2*x4 + 33*x2^2*x4 + 202*x1*x3*x4 + 202*x2*x3*x4 + 125*x3^2*x4 + 125*x1*x4^2 + 33*x2*x4^2 + 125*x3*x4^2 + 65388*x4^3 + 34*x1^2*x5 + 65455*x1*x2*x5 + 34*x2^2*x5 + 65505*x1*x3*x5 + 65455*x2*x3*x5 + 34*x3^2*x5 + 65455*x1*x4*x5 + 65505*x2*x4*x5 + 65455*x3*x4*x5 + 34*x4^2*x5 + 65503*x1*x5^2 + 65503*x2*x5^2 + 65503*x3*x5^2 + 65503*x4*x5^2 + 65508*x5^3 + 34*x1^2*x6 + 65455*x1*x2*x6 + 34*x2^2*x6 + 65505*x1*x3*x6 + 65455*x2*x3*x6 + 34*x3^2*x6 + 65455*x1*x4*x6 + 65505*x2*x4*x6 + 65455*x3*x4*x6 + 34*x4^2*x6 + 46*x1*x5*x6 + 46*x2*x5*x6 + 46*x3*x5*x6 + 46*x4*x5*x6 + 33358*x5^2*x6 + 65503*x1*x6^2 + 65503*x2*x6^2 + 65503*x3*x6^2 + 65503*x4*x6^2 + 32309*x5*x6^2 + 65508*x6^3 + 34*x1^2*x7 + 65455*x1*x2*x7 + 34*x2^2*x7 + 65505*x1*x3*x7 + 65455*x2*x3*x7 + 34*x3^2*x7 + 65455*x1*x4*x7 + 65505*x2*x4*x7 + 65455*x3*x4*x7 + 34*x4^2*x7 + 112*x1*x5*x7 + 112*x2*x5*x7 + 112*x3*x5*x7 + 112*x4*x5*x7 + 149*x5^2*x7 + 46*x1*x6*x7 + 46*x2*x6*x7 + 46*x3*x6*x7 + 46*x4*x6*x7 + 310*x5*x6*x7 + 33358*x6^2*x7 + 65503*x1*x7^2 + 65503*x2*x7^2 + 65503*x3*x7^2 + 65503*x4*x7^2 + 149*x5*x7^2 + 32309*x6*x7^2 + 65508*x7^3 + 34*x1^2*x8 + 65455*x1*x2*x8 + 34*x2^2*x8 + 65505*x1*x3*x8 + 65455*x2*x3*x8 + 34*x3^2*x8 + 65455*x1*x4*x8 + 65505*x2*x4*x8 + 65455*x3*x4*x8 + 34*x4^2*x8 + 46*x1*x5*x8 + 46*x2*x5*x8 + 46*x3*x5*x8 + 46*x4*x5*x8 + 32309*x5^2*x8 + 112*x1*x6*x8 + 112*x2*x6*x8 + 112*x3*x6*x8 + 112*x4*x6*x8 + 310*x5*x6*x8 + 149*x6^2*x8 + 46*x1*x7*x8 + 46*x2*x7*x8 + 46*x3*x7*x8 + 46*x4*x7*x8 + 310*x5*x7*x8 + 310*x6*x7*x8 + 33358*x7^2*x8 + 65503*x1*x8^2 + 65503*x2*x8^2 + 65503*x3*x8^2 + 65503*x4*x8^2 + 33358*x5*x8^2 + 149*x6*x8^2 + 32309*x7*x8^2 + 65508*x8^3 + 31*x1^2 + 65411*x1*x2 + 31*x2^2 + 65447*x1*x3 + 65411*x2*x3 + 31*x3^2 + 65411*x1*x4 + 65447*x2*x4 + 65411*x3*x4 + 31*x4^2 + 30*x1*x5 + 30*x2*x5 + 30*x3*x5 + 30*x4*x5 + 65459*x5^2 + 30*x1*x6 + 30*x2*x6 + 30*x3*x6 + 30*x4*x6 + 65397*x5*x6 + 65459*x6^2 + 30*x1*x7 + 30*x2*x7 + 30*x3*x7 + 30*x4*x7 + 76*x5*x7 + 65397*x6*x7 + 65459*x7^2 + 30*x1*x8 + 30*x2*x8 + 30*x3*x8 + 30*x4*x8 + 65397*x5*x8 + 76*x6*x8 + 65397*x7*x8 + 65459*x8^2 + 45*x1 + 45*x2 + 45*x3 + 45*x4 + 31*x5 + 31*x6 + 31*x7 + 31*x8 + 54981, 65507*x1^3 + 1597*x1^2*x2 + 63704*x1*x2^2 + 65507*x2^3 + 65459*x1^2*x3 + 65225*x1*x2*x3 + 1597*x2^2*x3 + 65459*x1*x3^2 + 63704*x2*x3^2 + 65507*x3^3 + 63704*x1^2*x4 + 65225*x1*x2*x4 + 65459*x2^2*x4 + 65225*x1*x3*x4 + 65225*x2*x3*x4 + 1597*x3^2*x4 + 1597*x1*x4^2 + 65459*x2*x4^2 + 63704*x3*x4^2 + 65507*x4^3 + 65480*x1^2*x5 + 65455*x1*x2*x5 + 65480*x2^2*x5 + 65343*x1*x3*x5 + 65455*x2*x3*x5 + 65480*x3^2*x5 + 65455*x1*x4*x5 + 65343*x2*x4*x5 + 65455*x3*x4*x5 + 65480*x4^2*x5 + 95*x1*x5^2 + 95*x2*x5^2 + 95*x3*x5^2 + 95*x4*x5^2 + 42*x5^3 + 65480*x1^2*x6 + 65455*x1*x2*x6 + 65480*x2^2*x6 + 65343*x1*x3*x6 + 65455*x2*x3*x6 + 65480*x3^2*x6 + 65455*x1*x4*x6 + 65343*x2*x4*x6 + 65455*x3*x4*x6 + 65480*x4^2*x6 + 64*x1*x5*x6 + 64*x2*x5*x6 + 64*x3*x5*x6 + 64*x4*x5*x6 + 27359*x5^2*x6 + 95*x1*x6^2 + 95*x2*x6^2 + 95*x3*x6^2 + 95*x4*x6^2 + 38294*x5*x6^2 + 42*x6^3 + 65480*x1^2*x7 + 65455*x1*x2*x7 + 65480*x2^2*x7 + 65343*x1*x3*x7 + 65455*x2*x3*x7 + 65480*x3^2*x7 + 65455*x1*x4*x7 + 65343*x2*x4*x7 + 65455*x3*x4*x7 + 65480*x4^2*x7 + 50*x1*x5*x7 + 50*x2*x5*x7 + 50*x3*x5*x7 + 50*x4*x5*x7 + 65399*x5^2*x7 + 64*x1*x6*x7 + 64*x2*x6*x7 + 64*x3*x6*x7 + 64*x4*x6*x7 + 12*x5*x6*x7 + 27359*x6^2*x7 + 95*x1*x7^2 + 95*x2*x7^2 + 95*x3*x7^2 + 95*x4*x7^2 + 65399*x5*x7^2 + 38294*x6*x7^2 + 42*x7^3 + 65480*x1^2*x8 + 65455*x1*x2*x8 + 65480*x2^2*x8 + 65343*x1*x3*x8 + 65455*x2*x3*x8 + 65480*x3^2*x8 + 65455*x1*x4*x8 + 65343*x2*x4*x8 + 65455*x3*x4*x8 + 65480*x4^2*x8 + 64*x1*x5*x8 + 64*x2*x5*x8 + 64*x3*x5*x8 + 64*x4*x5*x8 + 38294*x5^2*x8 + 50*x1*x6*x8 + 50*x2*x6*x8 + 50*x3*x6*x8 + 50*x4*x6*x8 + 12*x5*x6*x8 + 65399*x6^2*x8 + 64*x1*x7*x8 + 64*x2*x7*x8 + 64*x3*x7*x8 + 64*x4*x7*x8 + 12*x5*x7*x8 + 12*x6*x7*x8 + 27359*x7^2*x8 + 95*x1*x8^2 + 95*x2*x8^2 + 95*x3*x8^2 + 95*x4*x8^2 + 27359*x5*x8^2 + 65399*x6*x8^2 + 38294*x7*x8^2 + 42*x8^3 + 10*x1^2 + 8*x1*x2 + 10*x2^2 + 65453*x1*x3 + 8*x2*x3 + 10*x3^2 + 8*x1*x4 + 65453*x2*x4 + 8*x3*x4 + 10*x4^2 + 65484*x1*x5 + 65484*x2*x5 + 65484*x3*x5 + 65484*x4*x5 + 65495*x5^2 + 65484*x1*x6 + 65484*x2*x6 + 65484*x3*x6 + 65484*x4*x6 + 36*x5*x6 + 65495*x6^2 + 65484*x1*x7 + 65484*x2*x7 + 65484*x3*x7 + 65484*x4*x7 + 65285*x5*x7 + 36*x6*x7 + 65495*x7^2 + 65484*x1*x8 + 65484*x2*x8 + 65484*x3*x8 + 65484*x4*x8 + 36*x5*x8 + 65285*x6*x8 + 36*x7*x8 + 65495*x8^2 + 65517*x1 + 65517*x2 + 65517*x3 + 65517*x4 + 10*x5 + 10*x6 + 10*x7 + 10*x8 + 16724, 6*x1^3 + 7264*x1^2*x2 + 58525*x1*x2^2 + 6*x2^3 + 110*x1^2*x3 + 368*x1*x2*x3 + 7264*x2^2*x3 + 110*x1*x3^2 + 58525*x2*x3^2 + 6*x3^3 + 58525*x1^2*x4 + 368*x1*x2*x4 + 110*x2^2*x4 + 368*x1*x3*x4 + 368*x2*x3*x4 + 7264*x3^2*x4 + 7264*x1*x4^2 + 110*x2*x4^2 + 58525*x3*x4^2 + 6*x4^3 + 24*x1^2*x5 + 20*x1*x2*x5 + 24*x2^2*x5 + 65449*x1*x3*x5 + 20*x2*x3*x5 + 24*x3^2*x5 + 20*x1*x4*x5 + 65449*x2*x4*x5 + 20*x3*x4*x5 + 24*x4^2*x5 + 65412*x1*x5^2 + 65412*x2*x5^2 + 65412*x3*x5^2 + 65412*x4*x5^2 + 65498*x5^3 + 24*x1^2*x6 + 20*x1*x2*x6 + 24*x2^2*x6 + 65449*x1*x3*x6 + 20*x2*x3*x6 + 24*x3^2*x6 + 20*x1*x4*x6 + 65449*x2*x4*x6 + 20*x3*x4*x6 + 24*x4^2*x6 + 65515*x1*x5*x6 + 65515*x2*x5*x6 + 65515*x3*x5*x6 + 65515*x4*x5*x6 + 27374*x5^2*x6 + 65412*x1*x6^2 + 65412*x2*x6^2 + 65412*x3*x6^2 + 65412*x4*x6^2 + 38309*x5*x6^2 + 65498*x6^3 + 24*x1^2*x7 + 20*x1*x2*x7 + 24*x2^2*x7 + 65449*x1*x3*x7 + 20*x2*x3*x7 + 24*x3^2*x7 + 20*x1*x4*x7 + 65449*x2*x4*x7 + 20*x3*x4*x7 + 24*x4^2*x7 + 65447*x1*x5*x7 + 65447*x2*x5*x7 + 65447*x3*x5*x7 + 65447*x4*x5*x7 + 31*x5^2*x7 + 65515*x1*x6*x7 + 65515*x2*x6*x7 + 65515*x3*x6*x7 + 65515*x4*x6*x7 + 65271*x5*x6*x7 + 27374*x6^2*x7 + 65412*x1*x7^2 + 65412*x2*x7^2 + 65412*x3*x7^2 + 65412*x4*x7^2 + 31*x5*x7^2 + 38309*x6*x7^2 + 65498*x7^3 + 24*x1^2*x8 + 20*x1*x2*x8 + 24*x2^2*x8 + 65449*x1*x3*x8 + 20*x2*x3*x8 + 24*x3^2*x8 + 20*x1*x4*x8 + 65449*x2*x4*x8 + 20*x3*x4*x8 + 24*x4^2*x8 + 65515*x1*x5*x8 + 65515*x2*x5*x8 + 65515*x3*x5*x8 + 65515*x4*x5*x8 + 38309*x5^2*x8 + 65447*x1*x6*x8 + 65447*x2*x6*x8 + 65447*x3*x6*x8 + 65447*x4*x6*x8 + 65271*x5*x6*x8 + 31*x6^2*x8 + 65515*x1*x7*x8 + 65515*x2*x7*x8 + 65515*x3*x7*x8 + 65515*x4*x7*x8 + 65271*x5*x7*x8 + 65271*x6*x7*x8 + 27374*x7^2*x8 + 65412*x1*x8^2 + 65412*x2*x8^2 + 65412*x3*x8^2 + 65412*x4*x8^2 + 27374*x5*x8^2 + 31*x6*x8^2 + 38309*x7*x8^2 + 65498*x8^3 + 126*x1^2 + 65503*x1*x2 + 126*x2^2 + 88*x1*x3 + 65503*x2*x3 + 126*x3^2 + 65503*x1*x4 + 88*x2*x4 + 65503*x3*x4 + 126*x4^2 + 33*x1*x5 + 33*x2*x5 + 33*x3*x5 + 33*x4*x5 + 33*x5^2 + 33*x1*x6 + 33*x2*x6 + 33*x3*x6 + 33*x4*x6 + 68*x5*x6 + 33*x6^2 + 33*x1*x7 + 33*x2*x7 + 33*x3*x7 + 33*x4*x7 + 65407*x5*x7 + 68*x6*x7 + 33*x7^2 + 33*x1*x8 + 33*x2*x8 + 33*x3*x8 + 33*x4*x8 + 68*x5*x8 + 65407*x6*x8 + 68*x7*x8 + 33*x8^2 + 35*x1 + 35*x2 + 35*x3 + 35*x4 + 45*x5 + 45*x6 + 45*x7 + 45*x8 + 43729, 65471*x1^3 + 27115*x1^2*x2 + 38050*x1*x2^2 + 65471*x2^3 + 106*x1^2*x3 + 65277*x1*x2*x3 + 27115*x2^2*x3 + 106*x1*x3^2 + 38050*x2*x3^2 + 65471*x3^3 + 38050*x1^2*x4 + 65277*x1*x2*x4 + 106*x2^2*x4 + 65277*x1*x3*x4 + 65277*x2*x3*x4 + 27115*x3^2*x4 + 27115*x1*x4^2 + 106*x2*x4^2 + 38050*x3*x4^2 + 65471*x4^3 + 46*x1^2*x5 + 65459*x1*x2*x5 + 46*x2^2*x5 + 16*x1*x3*x5 + 65459*x2*x3*x5 + 46*x3^2*x5 + 65459*x1*x4*x5 + 16*x2*x4*x5 + 65459*x3*x4*x5 + 46*x4^2*x5 + 65492*x1*x5^2 + 65492*x2*x5^2 + 65492*x3*x5^2 + 65492*x4*x5^2 + 22*x5^3 + 46*x1^2*x6 + 65459*x1*x2*x6 + 46*x2^2*x6 + 16*x1*x3*x6 + 65459*x2*x3*x6 + 46*x3^2*x6 + 65459*x1*x4*x6 + 16*x2*x4*x6 + 65459*x3*x4*x6 + 46*x4^2*x6 + 158*x1*x5*x6 + 158*x2*x5*x6 + 158*x3*x5*x6 + 158*x4*x5*x6 + 21245*x5^2*x6 + 65492*x1*x6^2 + 65492*x2*x6^2 + 65492*x3*x6^2 + 65492*x4*x6^2 + 44164*x5*x6^2 + 22*x6^3 + 46*x1^2*x7 + 65459*x1*x2*x7 + 46*x2^2*x7 + 16*x1*x3*x7 + 65459*x2*x3*x7 + 46*x3^2*x7 + 65459*x1*x4*x7 + 16*x2*x4*x7 + 65459*x3*x4*x7 + 46*x4^2*x7 + 22*x1*x5*x7 + 22*x2*x5*x7 + 22*x3*x5*x7 + 22*x4*x5*x7 + 26*x5^2*x7 + 158*x1*x6*x7 + 158*x2*x6*x7 + 158*x3*x6*x7 + 158*x4*x6*x7 + 65089*x5*x6*x7 + 21245*x6^2*x7 + 65492*x1*x7^2 + 65492*x2*x7^2 + 65492*x3*x7^2 + 65492*x4*x7^2 + 26*x5*x7^2 + 44164*x6*x7^2 + 22*x7^3 + 46*x1^2*x8 + 65459*x1*x2*x8 + 46*x2^2*x8 + 16*x1*x3*x8 + 65459*x2*x3*x8 + 46*x3^2*x8 + 65459*x1*x4*x8 + 16*x2*x4*x8 + 65459*x3*x4*x8 + 46*x4^2*x8 + 158*x1*x5*x8 + 158*x2*x5*x8 + 158*x3*x5*x8 + 158*x4*x5*x8 + 44164*x5^2*x8 + 22*x1*x6*x8 + 22*x2*x6*x8 + 22*x3*x6*x8 + 22*x4*x6*x8 + 65089*x5*x6*x8 + 26*x6^2*x8 + 158*x1*x7*x8 + 158*x2*x7*x8 + 158*x3*x7*x8 + 158*x4*x7*x8 + 65089*x5*x7*x8 + 65089*x6*x7*x8 + 21245*x7^2*x8 + 65492*x1*x8^2 + 65492*x2*x8^2 + 65492*x3*x8^2 + 65492*x4*x8^2 + 21245*x5*x8^2 + 26*x6*x8^2 + 44164*x7*x8^2 + 22*x8^3 + 65488*x1^2 + 72*x1*x2 + 65488*x2^2 + 65507*x1*x3 + 72*x2*x3 + 65488*x3^2 + 72*x1*x4 + 65507*x2*x4 + 72*x3*x4 + 65488*x4^2 + 20*x1*x5 + 20*x2*x5 + 20*x3*x5 + 20*x4*x5 + 12*x5^2 + 20*x1*x6 + 20*x2*x6 + 20*x3*x6 + 20*x4*x6 + 124*x5*x6 + 12*x6^2 + 20*x1*x7 + 20*x2*x7 + 20*x3*x7 + 20*x4*x7 + 65433*x5*x7 + 124*x6*x7 + 12*x7^2 + 20*x1*x8 + 20*x2*x8 + 20*x3*x8 + 20*x4*x8 + 124*x5*x8 + 65433*x6*x8 + 124*x7*x8 + 12*x8^2 + 65478*x1 + 65478*x2 + 65478*x3 + 65478*x4 + 65520*x5 + 65520*x6 + 65520*x7 + 65520*x8 + 26144 ] :