#vars [ x1, x2, x3, x4, x5, x6, x7, x8 ] #modulo 65521 #list [ 65281*x1^3 + 59794*x1^2*x2 + 50338*x1*x2^2 + 65281*x2^3 + 38492*x1^2*x3 + 19629*x1*x2*x3 + 59794*x2^2*x3 + 26597*x1*x3^2 + 50338*x2*x3^2 + 65281*x3^3 + 39717*x1^2*x4 + 61199*x1*x2*x4 + 38492*x2^2*x4 + 4058*x1*x3*x4 + 19629*x2*x3*x4 + 59794*x3^2*x4 + 46886*x1*x4^2 + 26597*x2*x4^2 + 50338*x3*x4^2 + 65281*x4^3 + 65461*x1^2*x5 + 22557*x1*x2*x5 + 39717*x2^2*x5 + 65069*x1*x3*x5 + 61199*x2*x3*x5 + 38492*x3^2*x5 + 43200*x1*x4*x5 + 4058*x2*x4*x5 + 19629*x3*x4*x5 + 59794*x4^2*x5 + 65461*x1*x5^2 + 46886*x2*x5^2 + 26597*x3*x5^2 + 50338*x4*x5^2 + 65281*x5^3 + 46886*x1^2*x6 + 43200*x1*x2*x6 + 65461*x2^2*x6 + 45332*x1*x3*x6 + 22557*x2*x3*x6 + 39717*x3^2*x6 + 45332*x1*x4*x6 + 65069*x2*x4*x6 + 61199*x3*x4*x6 + 38492*x4^2*x6 + 22557*x1*x5*x6 + 43200*x2*x5*x6 + 4058*x3*x5*x6 + 19629*x4*x5*x6 + 59794*x5^2*x6 + 39717*x1*x6^2 + 65461*x2*x6^2 + 46886*x3*x6^2 + 26597*x4*x6^2 + 50338*x5*x6^2 + 65281*x6^3 + 26597*x1^2*x7 + 4058*x1*x2*x7 + 46886*x2^2*x7 + 65069*x1*x3*x7 + 43200*x2*x3*x7 + 65461*x3^2*x7 + 45332*x1*x4*x7 + 45332*x2*x4*x7 + 22557*x3*x4*x7 + 39717*x4^2*x7 + 65069*x1*x5*x7 + 45332*x2*x5*x7 + 65069*x3*x5*x7 + 61199*x4*x5*x7 + 38492*x5^2*x7 + 61199*x1*x6*x7 + 22557*x2*x6*x7 + 43200*x3*x6*x7 + 4058*x4*x6*x7 + 19629*x5*x6*x7 + 59794*x6^2*x7 + 38492*x1*x7^2 + 39717*x2*x7^2 + 65461*x3*x7^2 + 46886*x4*x7^2 + 26597*x5*x7^2 + 50338*x6*x7^2 + 65281*x7^3 + 50338*x1^2*x8 + 19629*x1*x2*x8 + 26597*x2^2*x8 + 61199*x1*x3*x8 + 4058*x2*x3*x8 + 46886*x3^2*x8 + 22557*x1*x4*x8 + 65069*x2*x4*x8 + 43200*x3*x4*x8 + 65461*x4^2*x8 + 43200*x1*x5*x8 + 45332*x2*x5*x8 + 45332*x3*x5*x8 + 22557*x4*x5*x8 + 39717*x5^2*x8 + 4058*x1*x6*x8 + 65069*x2*x6*x8 + 45332*x3*x6*x8 + 65069*x4*x6*x8 + 61199*x5*x6*x8 + 38492*x6^2*x8 + 19629*x1*x7*x8 + 61199*x2*x7*x8 + 22557*x3*x7*x8 + 43200*x4*x7*x8 + 4058*x5*x7*x8 + 19629*x6*x7*x8 + 59794*x7^2*x8 + 59794*x1*x8^2 + 38492*x2*x8^2 + 39717*x3*x8^2 + 65461*x4*x8^2 + 46886*x5*x8^2 + 26597*x6*x8^2 + 50338*x7*x8^2 + 65281*x8^3 + 6*x1^2 + 7624*x1*x2 + 6*x2^2 + 30*x1*x3 + 7624*x2*x3 + 6*x3^2 + 57941*x1*x4 + 30*x2*x4 + 7624*x3*x4 + 6*x4^2 + 65249*x1*x5 + 57941*x2*x5 + 30*x3*x5 + 7624*x4*x5 + 6*x5^2 + 57941*x1*x6 + 65249*x2*x6 + 57941*x3*x6 + 30*x4*x6 + 7624*x5*x6 + 6*x6^2 + 30*x1*x7 + 57941*x2*x7 + 65249*x3*x7 + 57941*x4*x7 + 30*x5*x7 + 7624*x6*x7 + 6*x7^2 + 7624*x1*x8 + 30*x2*x8 + 57941*x3*x8 + 65249*x4*x8 + 57941*x5*x8 + 30*x6*x8 + 7624*x7*x8 + 6*x8^2 + 9*x1 + 9*x2 + 9*x3 + 9*x4 + 9*x5 + 9*x6 + 9*x7 + 9*x8 + 10211, 85*x1^3 + 46966*x1^2*x2 + 4949*x1*x2^2 + 85*x2^3 + 30656*x1^2*x3 + 18332*x1*x2*x3 + 46966*x2^2*x3 + 34763*x1*x3^2 + 4949*x2*x3^2 + 85*x3^3 + 26868*x1^2*x4 + 46417*x1*x2*x4 + 30656*x2^2*x4 + 19424*x1*x3*x4 + 18332*x2*x3*x4 + 46966*x3^2*x4 + 52559*x1*x4^2 + 34763*x2*x4^2 + 4949*x3*x4^2 + 85*x4^3 + 65500*x1^2*x5 + 51264*x1*x2*x5 + 26868*x2^2*x5 + 65223*x1*x3*x5 + 46417*x2*x3*x5 + 30656*x3^2*x5 + 14085*x1*x4*x5 + 19424*x2*x4*x5 + 18332*x3*x4*x5 + 46966*x4^2*x5 + 65500*x1*x5^2 + 52559*x2*x5^2 + 34763*x3*x5^2 + 4949*x4*x5^2 + 85*x5^3 + 52559*x1^2*x6 + 14085*x1*x2*x6 + 65500*x2^2*x6 + 47653*x1*x3*x6 + 51264*x2*x3*x6 + 26868*x3^2*x6 + 47653*x1*x4*x6 + 65223*x2*x4*x6 + 46417*x3*x4*x6 + 30656*x4^2*x6 + 51264*x1*x5*x6 + 14085*x2*x5*x6 + 19424*x3*x5*x6 + 18332*x4*x5*x6 + 46966*x5^2*x6 + 26868*x1*x6^2 + 65500*x2*x6^2 + 52559*x3*x6^2 + 34763*x4*x6^2 + 4949*x5*x6^2 + 85*x6^3 + 34763*x1^2*x7 + 19424*x1*x2*x7 + 52559*x2^2*x7 + 65223*x1*x3*x7 + 14085*x2*x3*x7 + 65500*x3^2*x7 + 47653*x1*x4*x7 + 47653*x2*x4*x7 + 51264*x3*x4*x7 + 26868*x4^2*x7 + 65223*x1*x5*x7 + 47653*x2*x5*x7 + 65223*x3*x5*x7 + 46417*x4*x5*x7 + 30656*x5^2*x7 + 46417*x1*x6*x7 + 51264*x2*x6*x7 + 14085*x3*x6*x7 + 19424*x4*x6*x7 + 18332*x5*x6*x7 + 46966*x6^2*x7 + 30656*x1*x7^2 + 26868*x2*x7^2 + 65500*x3*x7^2 + 52559*x4*x7^2 + 34763*x5*x7^2 + 4949*x6*x7^2 + 85*x7^3 + 4949*x1^2*x8 + 18332*x1*x2*x8 + 34763*x2^2*x8 + 46417*x1*x3*x8 + 19424*x2*x3*x8 + 52559*x3^2*x8 + 51264*x1*x4*x8 + 65223*x2*x4*x8 + 14085*x3*x4*x8 + 65500*x4^2*x8 + 14085*x1*x5*x8 + 47653*x2*x5*x8 + 47653*x3*x5*x8 + 51264*x4*x5*x8 + 26868*x5^2*x8 + 19424*x1*x6*x8 + 65223*x2*x6*x8 + 47653*x3*x6*x8 + 65223*x4*x6*x8 + 46417*x5*x6*x8 + 30656*x6^2*x8 + 18332*x1*x7*x8 + 46417*x2*x7*x8 + 51264*x3*x7*x8 + 14085*x4*x7*x8 + 19424*x5*x7*x8 + 18332*x6*x7*x8 + 46966*x7^2*x8 + 46966*x1*x8^2 + 30656*x2*x8^2 + 26868*x3*x8^2 + 65500*x4*x8^2 + 52559*x5*x8^2 + 34763*x6*x8^2 + 4949*x7*x8^2 + 85*x8^3 + 26*x1^2 + 53133*x1*x2 + 26*x2^2 + 128*x1*x3 + 53133*x2*x3 + 26*x3^2 + 12228*x1*x4 + 128*x2*x4 + 53133*x3*x4 + 26*x4^2 + 172*x1*x5 + 12228*x2*x5 + 128*x3*x5 + 53133*x4*x5 + 26*x5^2 + 12228*x1*x6 + 172*x2*x6 + 12228*x3*x6 + 128*x4*x6 + 53133*x5*x6 + 26*x6^2 + 128*x1*x7 + 12228*x2*x7 + 172*x3*x7 + 12228*x4*x7 + 128*x5*x7 + 53133*x6*x7 + 26*x7^2 + 53133*x1*x8 + 128*x2*x8 + 12228*x3*x8 + 172*x4*x8 + 12228*x5*x8 + 128*x6*x8 + 53133*x7*x8 + 26*x8^2 + 6*x1 + 6*x2 + 6*x3 + 6*x4 + 6*x5 + 6*x6 + 6*x7 + 6*x8 + 20780, 65485*x1^3 + 19455*x1^2*x2 + 9897*x1*x2^2 + 65485*x2^3 + 14784*x1^2*x3 + 62609*x1*x2*x3 + 19455*x2^2*x3 + 50825*x1*x3^2 + 9897*x2*x3^2 + 65485*x3^3 + 26472*x1^2*x4 + 56569*x1*x2*x4 + 14784*x2^2*x4 + 7808*x1*x3*x4 + 62609*x2*x3*x4 + 19455*x3^2*x4 + 9037*x1*x4^2 + 50825*x2*x4^2 + 9897*x3*x4^2 + 65485*x4^3 + 65289*x1^2*x5 + 51860*x1*x2*x5 + 26472*x2^2*x5 + 65429*x1*x3*x5 + 56569*x2*x3*x5 + 14784*x3^2*x5 + 13721*x1*x4*x5 + 7808*x2*x4*x5 + 62609*x3*x4*x5 + 19455*x4^2*x5 + 65289*x1*x5^2 + 9037*x2*x5^2 + 50825*x3*x5^2 + 9897*x4*x5^2 + 65485*x5^3 + 9037*x1^2*x6 + 13721*x1*x2*x6 + 65289*x2^2*x6 + 2880*x1*x3*x6 + 51860*x2*x3*x6 + 26472*x3^2*x6 + 2880*x1*x4*x6 + 65429*x2*x4*x6 + 56569*x3*x4*x6 + 14784*x4^2*x6 + 51860*x1*x5*x6 + 13721*x2*x5*x6 + 7808*x3*x5*x6 + 62609*x4*x5*x6 + 19455*x5^2*x6 + 26472*x1*x6^2 + 65289*x2*x6^2 + 9037*x3*x6^2 + 50825*x4*x6^2 + 9897*x5*x6^2 + 65485*x6^3 + 50825*x1^2*x7 + 7808*x1*x2*x7 + 9037*x2^2*x7 + 65429*x1*x3*x7 + 13721*x2*x3*x7 + 65289*x3^2*x7 + 2880*x1*x4*x7 + 2880*x2*x4*x7 + 51860*x3*x4*x7 + 26472*x4^2*x7 + 65429*x1*x5*x7 + 2880*x2*x5*x7 + 65429*x3*x5*x7 + 56569*x4*x5*x7 + 14784*x5^2*x7 + 56569*x1*x6*x7 + 51860*x2*x6*x7 + 13721*x3*x6*x7 + 7808*x4*x6*x7 + 62609*x5*x6*x7 + 19455*x6^2*x7 + 14784*x1*x7^2 + 26472*x2*x7^2 + 65289*x3*x7^2 + 9037*x4*x7^2 + 50825*x5*x7^2 + 9897*x6*x7^2 + 65485*x7^3 + 9897*x1^2*x8 + 62609*x1*x2*x8 + 50825*x2^2*x8 + 56569*x1*x3*x8 + 7808*x2*x3*x8 + 9037*x3^2*x8 + 51860*x1*x4*x8 + 65429*x2*x4*x8 + 13721*x3*x4*x8 + 65289*x4^2*x8 + 13721*x1*x5*x8 + 2880*x2*x5*x8 + 2880*x3*x5*x8 + 51860*x4*x5*x8 + 26472*x5^2*x8 + 7808*x1*x6*x8 + 65429*x2*x6*x8 + 2880*x3*x6*x8 + 65429*x4*x6*x8 + 56569*x5*x6*x8 + 14784*x6^2*x8 + 62609*x1*x7*x8 + 56569*x2*x7*x8 + 51860*x3*x7*x8 + 13721*x4*x7*x8 + 7808*x5*x7*x8 + 62609*x6*x7*x8 + 19455*x7^2*x8 + 19455*x1*x8^2 + 14784*x2*x8^2 + 26472*x3*x8^2 + 65289*x4*x8^2 + 9037*x5*x8^2 + 50825*x6*x8^2 + 9897*x7*x8^2 + 65485*x8^3 + 72*x1^2 + 142*x1*x2 + 72*x2^2 + 88*x1*x3 + 142*x2*x3 + 72*x3^2 + 142*x1*x4 + 88*x2*x4 + 142*x3*x4 + 72*x4^2 + 65305*x1*x5 + 142*x2*x5 + 88*x3*x5 + 142*x4*x5 + 72*x5^2 + 142*x1*x6 + 65305*x2*x6 + 142*x3*x6 + 88*x4*x6 + 142*x5*x6 + 72*x6^2 + 88*x1*x7 + 142*x2*x7 + 65305*x3*x7 + 142*x4*x7 + 88*x5*x7 + 142*x6*x7 + 72*x7^2 + 142*x1*x8 + 88*x2*x8 + 142*x3*x8 + 65305*x4*x8 + 142*x5*x8 + 88*x6*x8 + 142*x7*x8 + 72*x8^2 + 65493*x1 + 65493*x2 + 65493*x3 + 65493*x4 + 65493*x5 + 65493*x6 + 65493*x7 + 65493*x8 + 9932, 65363*x1^3 + 129*x1^2*x2 + 36653*x1*x2^2 + 65363*x2^3 + 48740*x1^2*x3 + 10957*x1*x2*x3 + 129*x2^2*x3 + 17073*x1*x3^2 + 36653*x2*x3^2 + 65363*x3^3 + 3051*x1^2*x4 + 58165*x1*x2*x4 + 48740*x2^2*x4 + 6900*x1*x3*x4 + 10957*x2*x3*x4 + 129*x3^2*x4 + 25404*x1*x4^2 + 17073*x2*x4^2 + 36653*x3*x4^2 + 65363*x4^3 + 65323*x1^2*x5 + 30917*x1*x2*x5 + 3051*x2^2*x5 + 208*x1*x3*x5 + 58165*x2*x3*x5 + 48740*x3^2*x5 + 34064*x1*x4*x5 + 6900*x2*x4*x5 + 10957*x3*x4*x5 + 129*x4^2*x5 + 65323*x1*x5^2 + 25404*x2*x5^2 + 17073*x3*x5^2 + 36653*x4*x5^2 + 65363*x5^3 + 25404*x1^2*x6 + 34064*x1*x2*x6 + 65323*x2^2*x6 + 54036*x1*x3*x6 + 30917*x2*x3*x6 + 3051*x3^2*x6 + 54036*x1*x4*x6 + 208*x2*x4*x6 + 58165*x3*x4*x6 + 48740*x4^2*x6 + 30917*x1*x5*x6 + 34064*x2*x5*x6 + 6900*x3*x5*x6 + 10957*x4*x5*x6 + 129*x5^2*x6 + 3051*x1*x6^2 + 65323*x2*x6^2 + 25404*x3*x6^2 + 17073*x4*x6^2 + 36653*x5*x6^2 + 65363*x6^3 + 17073*x1^2*x7 + 6900*x1*x2*x7 + 25404*x2^2*x7 + 208*x1*x3*x7 + 34064*x2*x3*x7 + 65323*x3^2*x7 + 54036*x1*x4*x7 + 54036*x2*x4*x7 + 30917*x3*x4*x7 + 3051*x4^2*x7 + 208*x1*x5*x7 + 54036*x2*x5*x7 + 208*x3*x5*x7 + 58165*x4*x5*x7 + 48740*x5^2*x7 + 58165*x1*x6*x7 + 30917*x2*x6*x7 + 34064*x3*x6*x7 + 6900*x4*x6*x7 + 10957*x5*x6*x7 + 129*x6^2*x7 + 48740*x1*x7^2 + 3051*x2*x7^2 + 65323*x3*x7^2 + 25404*x4*x7^2 + 17073*x5*x7^2 + 36653*x6*x7^2 + 65363*x7^3 + 36653*x1^2*x8 + 10957*x1*x2*x8 + 17073*x2^2*x8 + 58165*x1*x3*x8 + 6900*x2*x3*x8 + 25404*x3^2*x8 + 30917*x1*x4*x8 + 208*x2*x4*x8 + 34064*x3*x4*x8 + 65323*x4^2*x8 + 34064*x1*x5*x8 + 54036*x2*x5*x8 + 54036*x3*x5*x8 + 30917*x4*x5*x8 + 3051*x5^2*x8 + 6900*x1*x6*x8 + 208*x2*x6*x8 + 54036*x3*x6*x8 + 208*x4*x6*x8 + 58165*x5*x6*x8 + 48740*x6^2*x8 + 10957*x1*x7*x8 + 58165*x2*x7*x8 + 30917*x3*x7*x8 + 34064*x4*x7*x8 + 6900*x5*x7*x8 + 10957*x6*x7*x8 + 129*x7^2*x8 + 129*x1*x8^2 + 48740*x2*x8^2 + 3051*x3*x8^2 + 65323*x4*x8^2 + 25404*x5*x8^2 + 17073*x6*x8^2 + 36653*x7*x8^2 + 65363*x8^3 + 65490*x1^2 + 60747*x1*x2 + 65490*x2^2 + 48*x1*x3 + 60747*x2*x3 + 65490*x3^2 + 4638*x1*x4 + 48*x2*x4 + 60747*x3*x4 + 65490*x4^2 + 238*x1*x5 + 4638*x2*x5 + 48*x3*x5 + 60747*x4*x5 + 65490*x5^2 + 4638*x1*x6 + 238*x2*x6 + 4638*x3*x6 + 48*x4*x6 + 60747*x5*x6 + 65490*x6^2 + 48*x1*x7 + 4638*x2*x7 + 238*x3*x7 + 4638*x4*x7 + 48*x5*x7 + 60747*x6*x7 + 65490*x7^2 + 60747*x1*x8 + 48*x2*x8 + 4638*x3*x8 + 238*x4*x8 + 4638*x5*x8 + 48*x6*x8 + 60747*x7*x8 + 65490*x8^2 + 65499*x1 + 65499*x2 + 65499*x3 + 65499*x4 + 65499*x5 + 65499*x6 + 65499*x7 + 65499*x8 + 46226, 65418*x1^3 + 19068*x1^2*x2 + 48668*x1*x2^2 + 65418*x2^3 + 28567*x1^2*x3 + 57190*x1*x2*x3 + 19068*x2^2*x3 + 37404*x1*x3^2 + 48668*x2*x3^2 + 65418*x3^3 + 18397*x1^2*x4 + 4136*x1*x2*x4 + 28567*x2^2*x4 + 62145*x1*x3*x4 + 57190*x2*x3*x4 + 19068*x3^2*x4 + 45721*x1*x4^2 + 37404*x2*x4^2 + 48668*x3*x4^2 + 65418*x4^3 + 65456*x1^2*x5 + 14429*x1*x2*x5 + 18397*x2^2*x5 + 454*x1*x3*x5 + 4136*x2*x3*x5 + 28567*x3^2*x5 + 51608*x1*x4*x5 + 62145*x2*x4*x5 + 57190*x3*x4*x5 + 19068*x4^2*x5 + 65456*x1*x5^2 + 45721*x2*x5^2 + 37404*x3*x5^2 + 48668*x4*x5^2 + 65418*x5^3 + 45721*x1^2*x6 + 51608*x1*x2*x6 + 65456*x2^2*x6 + 8323*x1*x3*x6 + 14429*x2*x3*x6 + 18397*x3^2*x6 + 8323*x1*x4*x6 + 454*x2*x4*x6 + 4136*x3*x4*x6 + 28567*x4^2*x6 + 14429*x1*x5*x6 + 51608*x2*x5*x6 + 62145*x3*x5*x6 + 57190*x4*x5*x6 + 19068*x5^2*x6 + 18397*x1*x6^2 + 65456*x2*x6^2 + 45721*x3*x6^2 + 37404*x4*x6^2 + 48668*x5*x6^2 + 65418*x6^3 + 37404*x1^2*x7 + 62145*x1*x2*x7 + 45721*x2^2*x7 + 454*x1*x3*x7 + 51608*x2*x3*x7 + 65456*x3^2*x7 + 8323*x1*x4*x7 + 8323*x2*x4*x7 + 14429*x3*x4*x7 + 18397*x4^2*x7 + 454*x1*x5*x7 + 8323*x2*x5*x7 + 454*x3*x5*x7 + 4136*x4*x5*x7 + 28567*x5^2*x7 + 4136*x1*x6*x7 + 14429*x2*x6*x7 + 51608*x3*x6*x7 + 62145*x4*x6*x7 + 57190*x5*x6*x7 + 19068*x6^2*x7 + 28567*x1*x7^2 + 18397*x2*x7^2 + 65456*x3*x7^2 + 45721*x4*x7^2 + 37404*x5*x7^2 + 48668*x6*x7^2 + 65418*x7^3 + 48668*x1^2*x8 + 57190*x1*x2*x8 + 37404*x2^2*x8 + 4136*x1*x3*x8 + 62145*x2*x3*x8 + 45721*x3^2*x8 + 14429*x1*x4*x8 + 454*x2*x4*x8 + 51608*x3*x4*x8 + 65456*x4^2*x8 + 51608*x1*x5*x8 + 8323*x2*x5*x8 + 8323*x3*x5*x8 + 14429*x4*x5*x8 + 18397*x5^2*x8 + 62145*x1*x6*x8 + 454*x2*x6*x8 + 8323*x3*x6*x8 + 454*x4*x6*x8 + 4136*x5*x6*x8 + 28567*x6^2*x8 + 57190*x1*x7*x8 + 4136*x2*x7*x8 + 14429*x3*x7*x8 + 51608*x4*x7*x8 + 62145*x5*x7*x8 + 57190*x6*x7*x8 + 19068*x7^2*x8 + 19068*x1*x8^2 + 28567*x2*x8^2 + 18397*x3*x8^2 + 65456*x4*x8^2 + 45721*x5*x8^2 + 37404*x6*x8^2 + 48668*x7*x8^2 + 65418*x8^3 + 106*x1^2 + 55957*x1*x2 + 106*x2^2 + 65453*x1*x3 + 55957*x2*x3 + 106*x3^2 + 9260*x1*x4 + 65453*x2*x4 + 55957*x3*x4 + 106*x4^2 + 20*x1*x5 + 9260*x2*x5 + 65453*x3*x5 + 55957*x4*x5 + 106*x5^2 + 9260*x1*x6 + 20*x2*x6 + 9260*x3*x6 + 65453*x4*x6 + 55957*x5*x6 + 106*x6^2 + 65453*x1*x7 + 9260*x2*x7 + 20*x3*x7 + 9260*x4*x7 + 65453*x5*x7 + 55957*x6*x7 + 106*x7^2 + 55957*x1*x8 + 65453*x2*x8 + 9260*x3*x8 + 20*x4*x8 + 9260*x5*x8 + 65453*x6*x8 + 55957*x7*x8 + 106*x8^2 + 17*x1 + 17*x2 + 17*x3 + 17*x4 + 17*x5 + 17*x6 + 17*x7 + 17*x8 + 13555, 50*x1^3 + 21760*x1^2*x2 + 31543*x1*x2^2 + 50*x2^3 + 36458*x1^2*x3 + 6694*x1*x2*x3 + 21760*x2^2*x3 + 28759*x1*x3^2 + 31543*x2*x3^2 + 50*x3^3 + 59743*x1^2*x4 + 46190*x1*x2*x4 + 36458*x2^2*x4 + 19631*x1*x3*x4 + 6694*x2*x3*x4 + 21760*x3^2*x4 + 18176*x1*x4^2 + 28759*x2*x4^2 + 31543*x3*x4^2 + 50*x4^3 + 65271*x1^2*x5 + 65023*x1*x2*x5 + 59743*x2^2*x5 + 88*x1*x3*x5 + 46190*x2*x3*x5 + 36458*x3^2*x5 + 462*x1*x4*x5 + 19631*x2*x4*x5 + 6694*x3*x4*x5 + 21760*x4^2*x5 + 65271*x1*x5^2 + 18176*x2*x5^2 + 28759*x3*x5^2 + 31543*x4*x5^2 + 50*x5^3 + 18176*x1^2*x6 + 462*x1*x2*x6 + 65271*x2^2*x6 + 59183*x1*x3*x6 + 65023*x2*x3*x6 + 59743*x3^2*x6 + 59183*x1*x4*x6 + 88*x2*x4*x6 + 46190*x3*x4*x6 + 36458*x4^2*x6 + 65023*x1*x5*x6 + 462*x2*x5*x6 + 19631*x3*x5*x6 + 6694*x4*x5*x6 + 21760*x5^2*x6 + 59743*x1*x6^2 + 65271*x2*x6^2 + 18176*x3*x6^2 + 28759*x4*x6^2 + 31543*x5*x6^2 + 50*x6^3 + 28759*x1^2*x7 + 19631*x1*x2*x7 + 18176*x2^2*x7 + 88*x1*x3*x7 + 462*x2*x3*x7 + 65271*x3^2*x7 + 59183*x1*x4*x7 + 59183*x2*x4*x7 + 65023*x3*x4*x7 + 59743*x4^2*x7 + 88*x1*x5*x7 + 59183*x2*x5*x7 + 88*x3*x5*x7 + 46190*x4*x5*x7 + 36458*x5^2*x7 + 46190*x1*x6*x7 + 65023*x2*x6*x7 + 462*x3*x6*x7 + 19631*x4*x6*x7 + 6694*x5*x6*x7 + 21760*x6^2*x7 + 36458*x1*x7^2 + 59743*x2*x7^2 + 65271*x3*x7^2 + 18176*x4*x7^2 + 28759*x5*x7^2 + 31543*x6*x7^2 + 50*x7^3 + 31543*x1^2*x8 + 6694*x1*x2*x8 + 28759*x2^2*x8 + 46190*x1*x3*x8 + 19631*x2*x3*x8 + 18176*x3^2*x8 + 65023*x1*x4*x8 + 88*x2*x4*x8 + 462*x3*x4*x8 + 65271*x4^2*x8 + 462*x1*x5*x8 + 59183*x2*x5*x8 + 59183*x3*x5*x8 + 65023*x4*x5*x8 + 59743*x5^2*x8 + 19631*x1*x6*x8 + 88*x2*x6*x8 + 59183*x3*x6*x8 + 88*x4*x6*x8 + 46190*x5*x6*x8 + 36458*x6^2*x8 + 6694*x1*x7*x8 + 46190*x2*x7*x8 + 65023*x3*x7*x8 + 462*x4*x7*x8 + 19631*x5*x7*x8 + 6694*x6*x7*x8 + 21760*x7^2*x8 + 21760*x1*x8^2 + 36458*x2*x8^2 + 59743*x3*x8^2 + 65271*x4*x8^2 + 18176*x5*x8^2 + 28759*x6*x8^2 + 31543*x7*x8^2 + 50*x8^3 + 65519*x1^2 + 1738*x1*x2 + 65519*x2^2 + 65395*x1*x3 + 1738*x2*x3 + 65519*x3^2 + 63639*x1*x4 + 65395*x2*x4 + 1738*x3*x4 + 65519*x4^2 + 65329*x1*x5 + 63639*x2*x5 + 65395*x3*x5 + 1738*x4*x5 + 65519*x5^2 + 63639*x1*x6 + 65329*x2*x6 + 63639*x3*x6 + 65395*x4*x6 + 1738*x5*x6 + 65519*x6^2 + 65395*x1*x7 + 63639*x2*x7 + 65329*x3*x7 + 63639*x4*x7 + 65395*x5*x7 + 1738*x6*x7 + 65519*x7^2 + 1738*x1*x8 + 65395*x2*x8 + 63639*x3*x8 + 65329*x4*x8 + 63639*x5*x8 + 65395*x6*x8 + 1738*x7*x8 + 65519*x8^2 + 23*x1 + 23*x2 + 23*x3 + 23*x4 + 23*x5 + 23*x6 + 23*x7 + 23*x8 + 44452, 65343*x1^3 + 33652*x1^2*x2 + 18723*x1*x2^2 + 65343*x2^3 + 22076*x1^2*x3 + 5307*x1*x2*x3 + 33652*x2^2*x3 + 42897*x1*x3^2 + 18723*x2*x3^2 + 65343*x3^3 + 34042*x1^2*x4 + 62214*x1*x2*x4 + 22076*x2^2*x4 + 3003*x1*x3*x4 + 5307*x2*x3*x4 + 33652*x3^2*x4 + 44397*x1*x4^2 + 42897*x2*x4^2 + 18723*x3*x4^2 + 65343*x4^3 + 206*x1^2*x5 + 59135*x1*x2*x5 + 34042*x2^2*x5 + 64793*x1*x3*x5 + 62214*x2*x3*x5 + 22076*x3^2*x5 + 5598*x1*x4*x5 + 3003*x2*x4*x5 + 5307*x3*x4*x5 + 33652*x4^2*x5 + 206*x1*x5^2 + 44397*x2*x5^2 + 42897*x3*x5^2 + 18723*x4*x5^2 + 65343*x5^3 + 44397*x1^2*x6 + 5598*x1*x2*x6 + 206*x2^2*x6 + 59966*x1*x3*x6 + 59135*x2*x3*x6 + 34042*x3^2*x6 + 59966*x1*x4*x6 + 64793*x2*x4*x6 + 62214*x3*x4*x6 + 22076*x4^2*x6 + 59135*x1*x5*x6 + 5598*x2*x5*x6 + 3003*x3*x5*x6 + 5307*x4*x5*x6 + 33652*x5^2*x6 + 34042*x1*x6^2 + 206*x2*x6^2 + 44397*x3*x6^2 + 42897*x4*x6^2 + 18723*x5*x6^2 + 65343*x6^3 + 42897*x1^2*x7 + 3003*x1*x2*x7 + 44397*x2^2*x7 + 64793*x1*x3*x7 + 5598*x2*x3*x7 + 206*x3^2*x7 + 59966*x1*x4*x7 + 59966*x2*x4*x7 + 59135*x3*x4*x7 + 34042*x4^2*x7 + 64793*x1*x5*x7 + 59966*x2*x5*x7 + 64793*x3*x5*x7 + 62214*x4*x5*x7 + 22076*x5^2*x7 + 62214*x1*x6*x7 + 59135*x2*x6*x7 + 5598*x3*x6*x7 + 3003*x4*x6*x7 + 5307*x5*x6*x7 + 33652*x6^2*x7 + 22076*x1*x7^2 + 34042*x2*x7^2 + 206*x3*x7^2 + 44397*x4*x7^2 + 42897*x5*x7^2 + 18723*x6*x7^2 + 65343*x7^3 + 18723*x1^2*x8 + 5307*x1*x2*x8 + 42897*x2^2*x8 + 62214*x1*x3*x8 + 3003*x2*x3*x8 + 44397*x3^2*x8 + 59135*x1*x4*x8 + 64793*x2*x4*x8 + 5598*x3*x4*x8 + 206*x4^2*x8 + 5598*x1*x5*x8 + 59966*x2*x5*x8 + 59966*x3*x5*x8 + 59135*x4*x5*x8 + 34042*x5^2*x8 + 3003*x1*x6*x8 + 64793*x2*x6*x8 + 59966*x3*x6*x8 + 64793*x4*x6*x8 + 62214*x5*x6*x8 + 22076*x6^2*x8 + 5307*x1*x7*x8 + 62214*x2*x7*x8 + 59135*x3*x7*x8 + 5598*x4*x7*x8 + 3003*x5*x7*x8 + 5307*x6*x7*x8 + 33652*x7^2*x8 + 33652*x1*x8^2 + 22076*x2*x8^2 + 34042*x3*x8^2 + 206*x4*x8^2 + 44397*x5*x8^2 + 42897*x6*x8^2 + 18723*x7*x8^2 + 65343*x8^3 + 23*x1^2 + 29678*x1*x2 + 23*x2^2 + 114*x1*x3 + 29678*x2*x3 + 23*x3^2 + 35831*x1*x4 + 114*x2*x4 + 29678*x3*x4 + 23*x4^2 + 22*x1*x5 + 35831*x2*x5 + 114*x3*x5 + 29678*x4*x5 + 23*x5^2 + 35831*x1*x6 + 22*x2*x6 + 35831*x3*x6 + 114*x4*x6 + 29678*x5*x6 + 23*x6^2 + 114*x1*x7 + 35831*x2*x7 + 22*x3*x7 + 35831*x4*x7 + 114*x5*x7 + 29678*x6*x7 + 23*x7^2 + 29678*x1*x8 + 114*x2*x8 + 35831*x3*x8 + 22*x4*x8 + 35831*x5*x8 + 114*x6*x8 + 29678*x7*x8 + 23*x8^2 + x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + 20001, 65490*x1^3 + 63759*x1^2*x2 + 42023*x1*x2^2 + 65490*x2^3 + 52927*x1^2*x3 + 5029*x1*x2*x3 + 63759*x2^2*x3 + 12512*x1*x3^2 + 42023*x2*x3^2 + 65490*x3^3 + 23009*x1^2*x4 + 45228*x1*x2*x4 + 52927*x2^2*x4 + 20305*x1*x3*x4 + 5029*x2*x3*x4 + 63759*x3^2*x4 + 2411*x1*x4^2 + 12512*x2*x4^2 + 42023*x3*x4^2 + 65490*x4^3 + 503*x1^2*x5 + 21461*x1*x2*x5 + 23009*x2^2*x5 + 65275*x1*x3*x5 + 45228*x2*x3*x5 + 52927*x3^2*x5 + 44380*x1*x4*x5 + 20305*x2*x4*x5 + 5029*x3*x4*x5 + 63759*x4^2*x5 + 503*x1*x5^2 + 2411*x2*x5^2 + 12512*x3*x5^2 + 42023*x4*x5^2 + 65490*x5^3 + 2411*x1^2*x6 + 44380*x1*x2*x6 + 503*x2^2*x6 + 61136*x1*x3*x6 + 21461*x2*x3*x6 + 23009*x3^2*x6 + 61136*x1*x4*x6 + 65275*x2*x4*x6 + 45228*x3*x4*x6 + 52927*x4^2*x6 + 21461*x1*x5*x6 + 44380*x2*x5*x6 + 20305*x3*x5*x6 + 5029*x4*x5*x6 + 63759*x5^2*x6 + 23009*x1*x6^2 + 503*x2*x6^2 + 2411*x3*x6^2 + 12512*x4*x6^2 + 42023*x5*x6^2 + 65490*x6^3 + 12512*x1^2*x7 + 20305*x1*x2*x7 + 2411*x2^2*x7 + 65275*x1*x3*x7 + 44380*x2*x3*x7 + 503*x3^2*x7 + 61136*x1*x4*x7 + 61136*x2*x4*x7 + 21461*x3*x4*x7 + 23009*x4^2*x7 + 65275*x1*x5*x7 + 61136*x2*x5*x7 + 65275*x3*x5*x7 + 45228*x4*x5*x7 + 52927*x5^2*x7 + 45228*x1*x6*x7 + 21461*x2*x6*x7 + 44380*x3*x6*x7 + 20305*x4*x6*x7 + 5029*x5*x6*x7 + 63759*x6^2*x7 + 52927*x1*x7^2 + 23009*x2*x7^2 + 503*x3*x7^2 + 2411*x4*x7^2 + 12512*x5*x7^2 + 42023*x6*x7^2 + 65490*x7^3 + 42023*x1^2*x8 + 5029*x1*x2*x8 + 12512*x2^2*x8 + 45228*x1*x3*x8 + 20305*x2*x3*x8 + 2411*x3^2*x8 + 21461*x1*x4*x8 + 65275*x2*x4*x8 + 44380*x3*x4*x8 + 503*x4^2*x8 + 44380*x1*x5*x8 + 61136*x2*x5*x8 + 61136*x3*x5*x8 + 21461*x4*x5*x8 + 23009*x5^2*x8 + 20305*x1*x6*x8 + 65275*x2*x6*x8 + 61136*x3*x6*x8 + 65275*x4*x6*x8 + 45228*x5*x6*x8 + 52927*x6^2*x8 + 5029*x1*x7*x8 + 45228*x2*x7*x8 + 21461*x3*x7*x8 + 44380*x4*x7*x8 + 20305*x5*x7*x8 + 5029*x6*x7*x8 + 63759*x7^2*x8 + 63759*x1*x8^2 + 52927*x2*x8^2 + 23009*x3*x8^2 + 503*x4*x8^2 + 2411*x5*x8^2 + 12512*x6*x8^2 + 42023*x7*x8^2 + 65490*x8^3 + 23*x1^2 + 11156*x1*x2 + 23*x2^2 + 65461*x1*x3 + 11156*x2*x3 + 23*x3^2 + 54233*x1*x4 + 65461*x2*x4 + 11156*x3*x4 + 23*x4^2 + 178*x1*x5 + 54233*x2*x5 + 65461*x3*x5 + 11156*x4*x5 + 23*x5^2 + 54233*x1*x6 + 178*x2*x6 + 54233*x3*x6 + 65461*x4*x6 + 11156*x5*x6 + 23*x6^2 + 65461*x1*x7 + 54233*x2*x7 + 178*x3*x7 + 54233*x4*x7 + 65461*x5*x7 + 11156*x6*x7 + 23*x7^2 + 11156*x1*x8 + 65461*x2*x8 + 54233*x3*x8 + 178*x4*x8 + 54233*x5*x8 + 65461*x6*x8 + 11156*x7*x8 + 23*x8^2 + 65508*x1 + 65508*x2 + 65508*x3 + 65508*x4 + 65508*x5 + 65508*x6 + 65508*x7 + 65508*x8 + 12996 ] :