Skip to content

Instantly share code, notes, and snippets.

@hellman

hellman/1_generate_pairs.py

Last active March 26, 2019 18:27
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save hellman/45406937a064597b6b85bd10c0920cb9 to your computer and use it in GitHub Desktop.
Save hellman/45406937a064597b6b85bd10c0920cb9 to your computer and use it in GitHub Desktop.
Download ZIP
0CTF 2019 Quals - zer0mi (Crypto 611 pts)
Raw
1_generate_pairs.py
#!/usr/bin/env sage
'''
Multivariate Public Key Cryptosystems by Jintai Ding et al., Chapter 2
Explains attack by Jacques Patarin.
The idea is to find a relation of plaintext-ciphertext bytes such that
when ciphertext is fixed, the relation is linear in plaintext.
Patarin showed that a sufficient amount of such relations exists.
'''
from sage.all import *
import re
F = GF(2**8, name='z8')
toF = F.fetch_int
fromF = lambda v: v.integer_representation()
if 0:
print "GO REAL"
s = open("output").read()
N = 63
f = open("data", "w")
DATA = N**2 + 100
PT = None
else:
print "GO LOCAL"
s = open("output_local").read()
N = 11
f = open("data_local", "w")
DATA = N**2 + 100
PT = map(toF, map(ord, "flag{abcde}"))
s = s.replace("[", "")
s = s.replace("]", "")
def parse_gf256(m):
s = m.group(1)
res = 0
for t in s.split(" + "):
if t == "1":
res ^= 1
elif t == "z8":
res ^= 2
else:
v, e = t.split("^")
assert v == "z8"
res ^= 2**int(e)
return str(res)
# parse polynomial..
pub = s.strip().splitlines()[:-1]
ct = s.strip().splitlines()[-1]
polys = []
strexp = []
for line in pub:
line = line.strip().strip(",")
strexp.append(line)
line = re.sub(r"\((.*?)\)", parse_gf256, line)
# print line
poly = []
for t in line.split(" + "):
parts = t.split("*")
cur = []
c = 1
try:
c = int(parts[0])
parts = parts[1:]
except:
pass
cur.append(c)
for p in parts:
assert p[0] == "x"
p = p[1:]
if p.endswith("^2"):
cur.append(int(p[:-2]))
cur.append(int(p[:-2]))
else:
cur.append(int(p))
poly.append(tuple(cur))
# print t, "->", cur
polys.append(tuple(poly))
def eval_poly(poly, xs):
out = 0
for t in poly:
res = toF(t[0])
res *= xs[t[1]]
res *= xs[t[2]]
out += res
return out
CT = [eval_poly(poly, PT) for poly in polys]
print "LOCAL FLAG ENCRYPTION:", ''.join(chr(fromF(x)) for x in CT).encode("hex"),
print "VS", ct
msg = map(toF, range(100, 100 + 2*N, 2))
for i in xrange(DATA):
if i % 16 == 0:
print "encrypt..", i
msg = [F.random_element() for _ in xrange(N)]
if 1: # if a part is known, that's good
# useful when Q is not irreducible..
msg[:5] = map(toF, map(ord, "flag{"))
res = [eval_poly(poly, msg) for poly in polys]
pt = ''.join(chr(fromF(x)) for x in msg)
ct = ''.join(chr(fromF(x)) for x in res)
f.write(pt.encode("hex") + " " + ct.encode("hex") + "\n")
f.flush()
Raw
2_solve.py
from sage.all import *
import re
F = GF(2**8, name='z8')
toF = F.fetch_int
fromF = lambda v: v.integer_representation()
if 0:
print "GO REAL"
s = open("data").read()
out = open("output").read()
N = 63
else:
print "GO LOCAL"
s = open("data_local").read()
out = open("output_local").read()
N = 11
PT = map(toF, map(ord, "flag{abcde}"))
CT = out.strip().splitlines()[-1].decode("hex")
CT = map(toF, map(ord, CT))
pairs = []
for line in s.strip().splitlines()[:4500]:
pt, ct = line.split()
pt = [toF(ord(ch)) for ch in pt.decode("hex")]
ct = [toF(ord(ch)) for ch in ct.decode("hex")]
pairs.append((pt, ct))
from itertools import product
VX = range(N)
VY = range(N, 2*N)
unknowns = []
unknowns += [()]
unknowns += list(map(tuple, Combinations(VX, 1))) # x_i
unknowns += list(map(tuple, Combinations(VY, 1))) # y_i
unknowns += list(map(tuple, product(VX, VY))) # x_i y_j
m = matrix(F, len(pairs), len(unknowns))
for ieq, (pt, ct) in enumerate(pairs):
inp = pt + ct
for i, unk in enumerate(unknowns):
if len(unk) == 0:
res = 1
elif len(unk) == 1:
res = inp[unk[0]]
else:
res = inp[unk[0]] * inp[unk[1]]
m[ieq,i] = res
print "first matrix..."
print m.nrows(), "x", m.ncols(), "rank", m.rank()
print
ct = CT
lineqs = []
target = []
# each row in kernel describes a relation on monomials
# that is true for all generated pairs
# by substituting y for known ciphertext, we get a linear equation on the plaintext!
for row in m.right_kernel().matrix():
vec = vector(F, N)
b = 0
for unk, coef in zip(unknowns, row):
if not coef: continue
if len(unk) == 0:
b += coef
elif len(unk) == 1:
vi = unk[0]
if vi < N:
vec[vi] += coef
elif N <= vi <= 2*N:
b += coef * ct[vi-N]
else:
assert 0
elif len(unk) == 2:
vi, vj = unk
assert vi < N
assert vj >= N
vec[vi] += coef * ct[vj-N]
lineqs.append(vec)
target.append(b)
m = matrix(F, lineqs)
print "second matrix..."
print m.nrows(), "x", m.ncols(), "rank", m.rank()
target = vector(F, target)
sol = m.solve_right(target)
print
print "Solutions:"
for z in m.right_kernel()[:500]:
print `"".join(chr(fromF(v)) for v in sol+z)`
print "2^%d" % (m.right_kernel().dimension() * 8), "solutions"
#flag{E$t-ce_qu3_Le_c!3l_m0uRra,_Mourr4_?}
Raw
encrypt.py
# Failed attempt with sage, so write my own
# Sorry for the slow implementation. If you want to test with smaller N you should change Polynomial.Q as well.
# Using pypy and a small th would also be helpful.
from os import urandom
from random import randrange
from fractions import gcd
from copy import copy, deepcopy
class NotImplemented(Exception):
pass
B = 8
class GF256(object):
def __init__(self, n=0):
assert n>=0 and n<256
self.v = []
for _ in range(B):
self.v.append(n%2)
n/=2
def int(self):
res = 0
for i in reversed(self.v):
res = res*2+i
return res
def __add__(self, x):
if isinstance(x, GF256):
res = deepcopy(self)
for i in range(B):
res.v[i] ^= x.v[i]
return res
else:
raise NotImplemented
def __mul__(self, x):
def mul2x(v, i):
v = [0]*i + v
for i in reversed(range(B, len(v))):
if v[i]!=0:
v[i]^=1
v[i-4]^=1
v[i-5]^=1
v[i-6]^=1
v[i-8]^=1
return v[:B]
if isinstance(x, GF256):
res = GF256()
for i in range(B):
if self.v[i]==0:
continue
tmp = mul2x(x.v, i)
for j in range(B):
res.v[j] ^= tmp[j]
return res
elif isinstance(x, Expression):
return x*self
else:
raise NotImplemented
def __repr__(self):
res = map(lambda (a,_):"z8^%d"%a if a>1 else "z8" if a==1 else "1", filter(lambda (_,a):a!=0, enumerate(self.v)))
if len(res)>0:
return ' + '.join(reversed(res))
else:
return '0'
N = 63
class Expression(object):
# For each term, we have at most two variables
# So we represent a*xi^b*xj^c as (a,i,b,j,c) (i<j),
# a*xi^b as (a,-1,-1,i,b),
# and a as (a,-1,-1,-1,-1)
def __init__(self, v=[]):
self.v = deepcopy(v)
@staticmethod
def cmp_term(t0, t1):
if t0[1]<t1[1]:
return 1
elif t0[1]>t1[1]:
return -1
elif t0[3]<t1[3]:
return 1
elif t0[3]>t1[3]:
return -1
elif t0[2]<t1[2]:
return 1
elif t0[2]>t1[2]:
return -1
elif t0[4]<t1[4]:
return 1
elif t0[4]>t1[4]:
return -1
else:
return 0
@staticmethod
def mult_term(t0, t1):
if t0[1]!=-1 or t1[1]!=-1:
raise NotImplemented
if t0[3]<t1[3]:
return (t0[0]*t1[0], t0[3], t0[4], t1[3], t1[4])
elif t0[3]>t1[3]:
return (t0[0]*t1[0], t1[3], t1[4], t0[3], t0[4])
else:
return (t0[0]*t1[0], -1, -1, t0[3], (t0[4]+t1[4])%255)
@staticmethod
def eliminate_term(ts):
res = []
v = [False]*len(ts)
for i in range(len(ts)):
if v[i]:
continue
coef = ts[i][0]
for j in range(i+1,len(ts)):
if ts[i][1]==ts[j][1] and ts[i][2]==ts[j][2] and ts[i][3]==ts[j][3] and ts[i][4]==ts[j][4]:
coef += ts[j][0]
v[j] = True
if coef.int()!=0:
res.append((coef,ts[i][1],ts[i][2],ts[i][3],ts[i][4]))
return res
@staticmethod
def repr_term(t):
coef = repr(t[0])
if coef=='0':
return coef
term = '('+coef+')*'
if t[1]!=-1:
term += 'x%d^%d*' % (t[1], t[2]) if t[2]!=1 else 'x%d*' % t[1]
if t[3]!=-1:
term += 'x%d^%d' % (t[3], t[4]) if t[4]!=1 else 'x%d' % t[3]
return term.strip('*')
def square(self):
res = []
for i in range(len(self.v)):
if self.v[i][1]!=-1:
raise NotImplemented
res.append((self.v[i][0]*self.v[i][0],-1,-1,self.v[i][3],(self.v[i][4]*2)%255))
return Expression(res)
def subs(self, x):
assert len(x)==N
res = GF256()
for t in self.v:
tmp = deepcopy(t[0])
for _ in range(t[2]):
tmp *= x[t[1]]
for _ in range(t[4]):
tmp *= x[t[3]]
res += tmp
return res
def __add__(self, x):
if isinstance(x, Expression):
res = []
i = 0
j = 0
while i<len(self.v) or j<len(x.v):
if i>=len(self.v):
res.append(copy(x.v[j]))
j+=1
continue
if j>=len(x.v):
res.append(copy(self.v[i]))
i+=1
continue
order = self.cmp_term(self.v[i],x.v[j])
if order==1:
res.append(copy(self.v[i]))
i+=1
elif order==-1:
res.append(copy(x.v[j]))
j+=1
else:
t0 = self.v[i]
t1 = x.v[j]
res.append((t0[0]+t1[0],t0[1],t0[2],t0[3],t0[4]))
i+=1
j+=1
return Expression(res)
else:
raise NotImplemented
def __mul__(self, x):
if isinstance(x, Expression):
res = []
for t0 in self.v:
for t1 in x.v:
res.append(self.mult_term(t0, t1))
res = self.eliminate_term(res)
return Expression(res)
elif isinstance(x, GF256):
res = []
for t0 in self.v:
res.append((t0[0]*x,t0[1],t0[2],t0[3],t0[4]))
return Expression(res)
else:
raise NotImplemented
def __repr__(self):
res = filter(lambda x:x!='0',map(self.repr_term, self.v))
if len(res)>0:
return ' + '.join(res)
else:
return '0'
class Polynomial(object):
# quotient as x^63 + z8^5*x^62 + (z8^7 + z8)*x^61 + z8*x^60 + (z8^7 + z8^6 + z8^5 + z8^4 + z8)*x^59 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x^58 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x^57 + (z8^7 + z8^6 + z8^3)*x^56 + (z8^3 + z8 + 1)*x^55 + (z8^4 + z8)*x^54 + (z8^5 + z8^3)*x^53 + (z8^7 + z8^6 + z8^2 + z8)*x^52 + (z8^5 + 1)*x^51 + (z8^6 + z8^2 + z8)*x^50 + (z8^5 + z8 + 1)*x^49 + (z8^5 + z8^4 + z8^3 + 1)*x^48 + (z8^7 + z8^3 + z8^2 + z8 + 1)*x^47 + (z8^7 + z8^6 + z8^5 + z8^3 + 1)*x^46 + z8^4*x^45 + (z8^3 + 1)*x^44 + (z8^4 + z8^2 + z8)*x^43 + (z8^5 + 1)*x^42 + (z8^5 + z8^4 + z8)*x^41 + (z8^7 + z8^5 + z8^2)*x^40 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x^39 + (z8^7 + z8^5 + z8^4 + z8^2)*x^38 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x^37 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x^36 + (z8^6 + z8^3 + 1)*x^35 + z8^3*x^34 + (z8^4 + z8^3 + z8^2)*x^33 + (z8^7 + z8^5 + z8)*x^32 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2)*x^31 + (z8^6 + z8^5 + 1)*x^30 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x^29 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x^28 + (z8^6 + z8^5 + z8^4 + z8^3)*x^27 + (z8^7 + z8^5 + z8^4 + 1)*x^26 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2)*x^25 + (z8^5 + z8^2 + z8 + 1)*x^24 + z8^7*x^23 + (z8^7 + z8^6 + z8)*x^22 + (z8^7 + 1)*x^21 + (z8^6 + z8^4 + z8^2)*x^20 + (z8^5 + 1)*x^19 + (z8^2 + 1)*x^18 + (z8^7 + z8^5 + z8^4 + z8^2 + z8 + 1)*x^17 + (z8^7 + z8^6 + z8^5 + z8^4)*x^16 + (z8^7 + z8^5 + z8^4 + z8^2 + z8)*x^15 + (z8^7 + z8^3 + z8)*x^14 + (z8^7 + z8^4 + z8^3 + z8)*x^13 + (z8^3 + z8^2 + 1)*x^12 + (z8^7 + z8^5 + z8^2)*x^11 + (z8^7 + z8^3 + z8 + 1)*x^10 + (z8^7 + z8^5 + z8^3 + 1)*x^9 + (z8^5 + z8^4 + z8^2 + z8)*x^8 + (z8^7 + z8^5 + z8^4 + z8^2 + z8 + 1)*x^7 + (z8^6 + z8^2 + 1)*x^6 + z8^6*x^5 + (z8^7 + z8)*x^4 + (z8^7 + z8^5 + z8^2)*x^3 + (z8^7 + z8^4)*x^2 + (z8^7 + z8^5 + z8^3)*x + z8^7
Q = map(lambda x:GF256(x), [128, 168, 144, 164, 130, 64, 69, 183, 54, 169, 139, 164, 13, 154, 138, 182, 240, 183, 5, 33, 84, 129, 194, 128, 39, 244, 177, 120, 254, 255, 97, 220, 162, 28, 8, 73, 254, 124, 180, 107, 164, 50, 33, 22, 9, 16, 233, 143, 57, 35, 70, 33, 198, 40, 18, 11, 200, 107, 107, 242, 2, 130, 32])
def __init__(self, v):
self.v = []
for i in range(N):
if i<len(v):
assert isinstance(v[i], Expression)
self.v.append(deepcopy(v[i]))
else:
self.v.append(Expression())
@staticmethod
def mod(v):
for i in reversed(range(N, len(v))):
for j in range(1, N+1):
v[i-j] += v[i]*Polynomial.Q[N-j]
return v[:N]
def export(self):
return deepcopy(self.v)
def square(self):
res = []
for i in range(N):
res.append(self.v[i].square())
res.append(Expression())
self.v = self.mod(res)
def __add__(self, x):
if isinstance(x, Polynomial):
res = deepcopy(self)
for i in range(N):
res.v[i] += x.v[i]
return res
else:
raise NotImplemented
def __mul__(self, x):
if isinstance(x, Polynomial):
res = []
for _ in range(2*N):
res.append(Expression())
for i in range(N):
for j in range(N):
res[i+j] += self.v[i]*x.v[j]
return Polynomial(self.mod(res))
else:
raise NotImplemented
def __repr__(self):
res = filter(lambda (_,x):x!='0',enumerate(map(repr, self.v)))
res = map(lambda (a,b):"(%s)*x^%d"%(b,a) if a>1 else "(%s)*x"%b if a==1 else b, reversed(res))
if len(res)>0:
return ' + '.join(res)
else:
return '0'
def gen_affine():
mat = []
for _ in range(N):
row = []
for _ in range(N):
row.append(GF256(randrange(0,256)))
mat.append(row)
# should check whether the matrix is inversible
return mat
def mat_mult(mat, vec):
assert len(mat)>0 and len(mat[0])==len(vec)
res = []
for i in range(len(mat)):
tmp = Expression()
for j in range(len(vec)):
tmp += mat[i][j]*vec[j]
res.append(tmp)
return res
def main():
# with open('flag') as f:
# flag = f.read()
a = map(lambda x:GF256(x), map(ord, flag)+map(ord, urandom(N-len(flag))))
q = 2**B
th = randrange(1,N)
while gcd(q**th+1,q**N-1)!=1:
th = randrange(1,N)
l1 = gen_affine()
l2 = gen_affine()
v = [Expression([(GF256(1),-1,-1,i,1)]) for i in range(N)]
v = mat_mult(l2, v)
p1 = Polynomial(v)
for i in range(B*th):
p1.square()
p = Polynomial(v)*p1
pubkey = mat_mult(l1, p.export())
print pubkey
ct = map(lambda x:x.subs(a), pubkey)
ct = ''.join(map(lambda x:chr(x.int()), ct))
print ct.encode('hex')
with open("output_local", "w") as f:
f.write(`pubkey`.replace(",",",\n")+"\n")
f.write(ct.encode('hex'))
# for local fast encryption
flag = "flag{abcde}"
N = 11
Polynomial.Q = Polynomial.Q[:N] # not irreducible probably, but still OK if we know some bytes of plaintext
if __name__ == '__main__':
main()
Raw
output_local
[(z8^7 + z8^6 + z8^3 + z8)*x0^2 + (z8^7 + z8^5 + z8^4 + 1)*x0*x1 + (z8^6 + z8^3 + z8 + 1)*x0*x2 + (z8^7 + z8^3)*x0*x3 + (z8^6 + z8^4 + z8^3 + z8)*x0*x4 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x5 + (z8^7 + z8^5 + z8^3 + z8^2 + z8)*x0*x6 + (z8^7 + z8^6)*x0*x7 + (z8^7 + z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x9 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3)*x1^2 + (z8^4 + z8^3 + 1)*x0*x10 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + z8 + 1)*x1^2 + (z8^3 + z8^2 + z8 + 1)*x1*x2 + (z8^5 + z8^4 + z8^3 + z8 + 1)*x1*x3 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x1*x4 + (z8^4 + z8^3 + z8^2 + z8 + 1)*x1*x5 + (z8^7 + z8^6 + z8^4 + z8^3 + 1)*x1*x6 + (z8^7 + z8^5 + z8^2 + z8 + 1)*x1*x7 + (z8^7 + z8^6 + z8^4 + z8^3 + z8)*x1*x8 + (z8^7 + z8^6 + z8^5 + z8^3 + z8)*x1*x9 + (z8^6 + z8^5 + z8^2 + z8)*x1*x10 + (z8^6 + z8^4 + z8^2 + z8)*x2^2 + (z8^7 + z8^5 + z8^4 + z8^3)*x2*x3 + (z8^5 + z8^4 + z8^3)*x2*x4 + (z8^5 + z8^4 + z8^2 + z8 + 1)*x2*x5 + (z8^7 + z8^5 + z8^2)*x2*x6 + (z8^5 + z8)*x2*x7 + (z8^7 + z8^4 + z8^3 + z8^2)*x2*x8 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x2*x9 + (z8^6 + z8^2 + 1)*x2*x10 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x3^2 + (z8^4 + z8^3 + z8^2)*x3*x4 + (z8^7 + z8^6 + z8^2 + 1)*x3*x5 + (z8^7 + z8^5 + z8^4 + z8^2 + z8)*x3*x6 + (z8^7 + z8^4 + z8^3)*x3*x7 + (z8^6 + z8^4 + z8 + 1)*x3*x8 + (z8^7 + z8^6 + z8^4 + z8^2 + z8)*x3*x9 + (z8^7 + z8^6 + z8^3 + z8^2 + 1)*x4^2 + (z8^6 + z8^3 + z8)*x3*x10 + (z8^7 + z8^3 + z8^2 + 1)*x4^2 + (z8^4 + z8^3 + z8^2 + z8 + 1)*x4*x5 + (z8^7 + z8^6 + z8^4 + z8)*x4*x6 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x4*x7 + (z8^6 + z8^3 + z8^2 + z8 + 1)*x4*x8 + (z8^3 + z8 + 1)*x4*x9 + (z8^7 + z8^3 + z8^2 + z8 + 1)*x4*x10 + (z8^7 + z8^2 + 1)*x5^2 + (z8^5 + z8^2)*x5*x6 + (z8^7 + z8^4 + z8^3 + z8^2 + 1)*x5*x7 + (z8^7 + z8^5 + z8^4 + z8^3)*x5*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2)*x5*x9 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x5*x10 + (z8^3 + 1)*x6^2 + (z8^7 + z8^5 + z8^3 + z8^2)*x6*x7 + (z8^6 + z8^5)*x6*x8 + (z8^5 + z8^4)*x6*x9 + (z8^7 + z8^5 + z8^3 + 1)*x6*x10 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8)*x7^2 + (z8^7 + z8^5 + z8^4 + z8^3 + 1)*x7*x8 + (z8^6 + z8^5 + z8 + 1)*x7*x9 + (z8^7 + z8^5 + z8^3 + z8^2 + z8 + 1)*x7*x10 + (z8^5 + z8)*x8^2 + (z8^7 + z8^2 + z8)*x8*x9 + (z8^6 + z8^5 + z8^3)*x8*x10 + (z8^4 + z8^2)*x9^2 + (z8^7 + z8^6 + z8)*x10^2 + (z8^7 + z8^6 + z8^2 + z8)*x9*x10 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x10^2,
(z8^5 + z8^3)*x0^2 + (z8^6 + z8^5 + z8^4 + z8^3 + z8)*x0*x1 + (z8^6 + z8^5 + z8^2)*x0*x2 + (z8^7 + z8^2 + z8 + 1)*x0*x3 + (z8^6 + z8^5 + z8^4 + 1)*x0*x4 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x0*x5 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x0*x6 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x0*x7 + (z8^5 + z8^3 + z8)*x0*x8 + (z8^6 + z8^5 + z8^4 + z8^3 + 1)*x0*x9 + (z8^7 + z8^4 + z8^3)*x1^2 + (z8^5 + z8^4 + z8^2)*x0*x10 + (z8^7 + z8^6 + z8^4 + z8^2 + z8 + 1)*x1^2 + (z8^7 + z8^6 + z8^3 + z8^2 + z8)*x1*x2 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + 1)*x1*x3 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x1*x4 + (z8^5 + z8^3 + 1)*x1*x5 + (z8^5 + z8^3 + 1)*x1*x6 + (z8^7 + z8^6 + z8^5 + z8^4 + 1)*x1*x7 + (z8^4 + 1)*x1*x8 + (z8^7 + z8^5 + z8 + 1)*x1*x9 + (z8^7 + z8^6 + 1)*x1*x10 + (z8^7 + z8^4 + z8^3)*x2^2 + (z8^7 + z8^4 + z8^3 + 1)*x2*x3 + (z8^7 + z8^6 + z8^5 + z8 + 1)*x2*x4 + (z8^6 + z8^4 + z8 + 1)*x2*x5 + (z8^6 + z8^5 + z8^4 + z8^3)*x2*x6 + (z8^4)*x2*x7 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + 1)*x2*x8 + (z8^5 + z8^4 + z8)*x2*x9 + (z8^7 + z8^4 + z8^2 + 1)*x2*x10 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x3^2 + (z8^4 + z8^3 + z8)*x3*x4 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2)*x3*x5 + (z8^7 + z8^6 + z8^5 + z8^3 + z8 + 1)*x3*x6 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + z8 + 1)*x3*x7 + (z8^6 + z8^5 + z8^4 + z8^3 + 1)*x3*x8 + (z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x3*x9 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x4^2 + (z8^7 + z8^3 + z8^2 + z8)*x3*x10 + (z8^4 + z8)*x4^2 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x4*x5 + (z8^7 + z8^6 + z8^3 + z8^2 + 1)*x4*x6 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x4*x7 + (z8^2)*x4*x8 + (z8^7 + z8^4 + z8^2 + 1)*x4*x9 + (z8^6 + z8^4 + z8 + 1)*x4*x10 + (z8^6 + z8^4)*x5^2 + (z8^6 + z8^5 + z8)*x5*x6 + (z8^7 + z8^6 + z8^2 + z8 + 1)*x5*x7 + (z8^5)*x5*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8)*x5*x9 + (z8^6 + z8^3 + z8^2 + 1)*x5*x10 + (z8^7 + z8^5 + z8^4 + z8^2 + z8)*x6^2 + (z8^7 + z8^5 + z8 + 1)*x6*x7 + (z8^7 + z8^5 + z8^4 + z8)*x6*x8 + (z8^3 + z8^2 + 1)*x6*x9 + (z8^6 + z8^4 + z8^3 + z8)*x6*x10 + (z8^2 + 1)*x7^2 + (z8^5 + z8^4)*x7*x8 + (z8^2)*x7*x9 + (z8^5 + z8 + 1)*x7*x10 + (z8^4 + z8^3 + z8^2 + z8 + 1)*x8^2 + (z8^7 + z8^6 + z8^5 + 1)*x8*x9 + (z8^7 + z8^6 + z8^5 + z8^4 + z8 + 1)*x8*x10 + (z8^7 + z8^5 + z8^4 + z8^3 + 1)*x9^2 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + z8)*x10^2 + (z8^6 + z8^5 + z8^3 + z8^2 + z8 + 1)*x9*x10 + (z8^7 + z8^4 + z8^3 + 1)*x10^2,
(z8^7 + z8^6 + z8^5 + z8^3 + z8)*x0^2 + (z8^3 + z8^2)*x0*x1 + (z8^6 + z8^5 + z8^2 + z8)*x0*x2 + (z8^6 + z8^2 + z8)*x0*x3 + (z8^6 + z8^5 + z8^4 + z8^3 + z8)*x0*x4 + (z8^7 + z8^4 + z8^3 + z8 + 1)*x0*x5 + (z8^6 + z8^4 + z8^3 + z8^2)*x0*x6 + (z8^6 + z8^4 + z8^2 + z8)*x0*x7 + (z8^6 + z8^2 + z8 + 1)*x0*x8 + (z8^7 + z8^5 + z8^3 + z8 + 1)*x0*x9 + (z8)*x1^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8)*x0*x10 + (z8^4 + z8^3)*x1^2 + (z8^7 + z8^6 + z8^5 + z8)*x1*x2 + (z8^7 + z8^6 + z8^4 + z8^2 + 1)*x1*x3 + (z8^4 + z8 + 1)*x1*x4 + (z8^6 + z8^5 + z8^2 + z8 + 1)*x1*x5 + (z8^7 + z8^3 + z8^2 + z8 + 1)*x1*x6 + (z8^5 + z8)*x1*x7 + (z8^6 + z8^4 + z8^3 + z8 + 1)*x1*x8 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x1*x9 + (z8^6 + z8^5 + z8^4 + z8^2 + 1)*x1*x10 + (z8^4 + z8^3 + z8)*x2^2 + (z8^7 + z8^6 + z8^5 + z8^2)*x2*x3 + (z8^7 + z8^5 + z8^3 + z8^2 + 1)*x2*x4 + (z8^6 + z8^5 + z8^3 + z8^2 + z8 + 1)*x2*x5 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2)*x2*x6 + (z8^6 + z8^5 + z8^3)*x2*x7 + (z8^7 + z8^5 + 1)*x2*x8 + (z8^7 + z8^3)*x2*x9 + (z8^7 + z8^6 + z8^5 + 1)*x2*x10 + (z8^6 + z8^2 + z8)*x3^2 + (z8^7 + z8^6 + z8^4 + z8^2)*x3*x4 + (z8^6 + z8^4 + z8^3)*x3*x5 + (z8^7 + z8^6 + 1)*x3*x6 + (z8^6 + z8^5 + z8^4 + z8^3 + 1)*x3*x7 + (z8^7 + z8^4 + z8 + 1)*x3*x8 + (z8^5 + z8^4 + z8)*x3*x9 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + 1)*x4^2 + (z8^7 + z8^5 + z8^4 + z8^3)*x3*x10 + (z8^7 + z8^6 + z8^5 + z8^3 + z8 + 1)*x4^2 + (z8^7 + z8^3 + z8 + 1)*x4*x5 + (z8^7 + z8^6 + z8^5 + z8^2 + z8)*x4*x6 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + z8 + 1)*x4*x7 + (z8^6 + z8^4 + z8^2 + z8)*x4*x8 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2)*x4*x9 + (z8^7 + z8^5 + z8^4 + 1)*x4*x10 + (z8^6 + z8^4 + z8^3 + z8^2 + 1)*x5^2 + (z8^7 + z8^5 + z8^4 + z8 + 1)*x5*x6 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x5*x7 + (z8^3)*x5*x8 + (z8 + 1)*x5*x9 + (z8^7 + z8^4 + z8^3 + z8 + 1)*x5*x10 + (z8^6 + z8^3 + z8^2 + 1)*x6^2 + (z8^7 + z8^5 + z8^3 + z8)*x6*x7 + (z8^7 + z8^5 + z8^3)*x6*x8 + (z8^6 + z8^3 + z8^2 + z8 + 1)*x6*x9 + (z8^7 + z8^4 + z8 + 1)*x6*x10 + (z8^6 + z8^5 + z8^2 + z8)*x7^2 + (z8^7 + z8^6 + z8^4 + z8^3 + z8 + 1)*x7*x8 + (z8^4 + z8^2 + 1)*x7*x9 + (z8^6 + z8^5 + z8^3 + 1)*x7*x10 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x8^2 + (z8^7 + z8^4 + z8^2)*x8*x9 + (z8^5 + z8^4 + z8^3 + z8 + 1)*x8*x10 + (z8^6 + z8^3 + z8^2 + z8 + 1)*x9^2 + (z8^7 + z8^4 + 1)*x10^2 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + 1)*x9*x10 + (z8^2 + z8)*x10^2,
(z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x0^2 + (z8^7 + z8^6 + z8^5 + 1)*x0*x1 + (z8^6 + z8^5 + z8^3 + z8^2)*x0*x2 + (z8^7 + z8^6 + z8^5 + z8)*x0*x3 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x0*x4 + (z8^7 + z8^3 + z8 + 1)*x0*x5 + (z8^7 + z8^5 + z8^4 + z8^2 + 1)*x0*x6 + (z8^6 + z8^5 + z8^4 + z8^3)*x0*x7 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + z8)*x0*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + 1)*x0*x9 + (z8^7 + z8^4 + z8^2 + z8)*x1^2 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x0*x10 + (z8^5 + 1)*x1^2 + (z8^6)*x1*x2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x1*x3 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x1*x4 + (z8^5 + z8^2)*x1*x5 + (z8^7 + z8^6 + z8^5 + z8)*x1*x6 + (z8^6 + z8^4 + z8^2)*x1*x7 + (z8^4 + z8^3 + 1)*x1*x8 + (z8^7 + z8^5 + z8^4 + z8^3 + z8)*x1*x9 + (z8^5 + z8^4 + z8^3 + z8)*x1*x10 + (z8^5 + z8^4 + z8^3)*x2^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x2*x3 + (z8^6 + z8^5 + z8^3 + z8^2)*x2*x4 + (z8^6 + z8^4 + z8^3 + z8^2 + 1)*x2*x5 + (z8^6 + z8^2 + 1)*x2*x6 + (z8^5 + z8^4 + z8^3 + z8)*x2*x7 + (z8^4 + z8^3 + z8^2 + z8)*x2*x8 + (z8^7 + z8^5 + z8^3)*x2*x9 + (z8^7 + z8^6 + z8^4 + z8)*x2*x10 + (z8^7 + z8^5 + z8^3 + z8^2 + z8 + 1)*x3^2 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x3*x4 + (z8^7 + z8^6 + z8^5 + z8^2 + z8 + 1)*x3*x5 + (z8^6 + z8^3 + z8 + 1)*x3*x6 + (z8^2 + z8)*x3*x7 + (z8^7 + z8^6 + z8^4 + z8^2 + 1)*x3*x8 + (z8^7 + z8^4 + z8^3 + z8)*x3*x9 + (z8^7 + z8^5 + z8^4)*x4^2 + (z8^7 + z8^4 + z8^3 + 1)*x3*x10 + (z8^5 + z8)*x4^2 + (z8^7 + z8^4 + z8^3 + 1)*x4*x5 + (z8^6 + z8^5 + z8^4 + z8^3)*x4*x6 + (z8^7 + z8^4 + z8^3 + z8^2 + 1)*x4*x7 + (z8^7 + z8^6 + z8^5 + z8^2 + z8)*x4*x8 + (z8^7 + z8^6 + z8^5)*x4*x9 + (z8^5 + z8^3 + z8^2 + z8 + 1)*x4*x10 + (z8^6 + z8^4 + z8^3 + z8^2)*x5^2 + (z8^7 + z8^5 + z8^2 + z8)*x5*x6 + (z8^6 + z8^4 + z8^3 + z8^2 + z8)*x5*x7 + (z8^7 + z8^5 + z8^4 + z8^2)*x5*x8 + (z8^3 + z8^2 + z8 + 1)*x5*x9 + (z8^6 + z8^5 + z8^4 + z8^2 + z8 + 1)*x5*x10 + (z8^5 + z8^3 + z8^2)*x6^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x6*x7 + (z8)*x6*x8 + (z8^6 + z8^4 + z8^3 + z8^2 + z8)*x6*x9 + (z8^5 + z8^4 + z8^3 + z8 + 1)*x6*x10 + (z8^7 + z8^4 + 1)*x7^2 + (z8^7 + z8^5 + z8^4 + z8)*x7*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8)*x7*x9 + (z8^3 + z8 + 1)*x7*x10 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2)*x8^2 + (z8^7 + z8^6 + z8^2 + z8 + 1)*x8*x9 + (z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x8*x10 + (z8^5 + z8^2 + 1)*x9^2 + (z8^7 + z8^5 + z8^2)*x10^2 + (z8^7 + z8^5 + z8^4 + z8 + 1)*x9*x10 + (z8^6 + z8^4 + z8^3 + z8)*x10^2,
(z8^7 + z8^6 + z8^5 + z8^4 + 1)*x0^2 + (z8^7 + z8^5 + z8^3 + z8)*x0*x1 + (z8^6 + z8^2 + 1)*x0*x2 + (z8^7 + z8^4 + z8^2 + 1)*x0*x3 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x0*x4 + (z8^6 + z8^5 + z8^4 + z8^2)*x0*x5 + (z8^7 + z8^6 + z8^5 + z8^3 + z8 + 1)*x0*x6 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2)*x0*x7 + (z8^7 + z8^6 + z8^4 + z8^2)*x0*x8 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2)*x0*x9 + (z8^7 + z8^5 + 1)*x1^2 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + 1)*x0*x10 + (z8^6 + z8^4 + z8^3 + z8^2)*x1^2 + (z8^6 + z8^5 + z8^4 + z8^3 + 1)*x1*x2 + (z8^5 + 1)*x1*x3 + (z8^2)*x1*x4 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + z8)*x1*x5 + (z8^7)*x1*x6 + (z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x1*x7 + (z8^7 + z8^5 + 1)*x1*x8 + (z8^6 + z8^2 + z8 + 1)*x1*x9 + (z8^7 + z8^5)*x1*x10 + (z8^2 + 1)*x2^2 + (z8^5 + z8^4 + z8^2)*x2*x3 + (z8^7 + z8^5 + z8^4 + z8^3)*x2*x4 + (z8^6 + z8^3 + z8 + 1)*x2*x5 + (z8^6 + z8^5 + z8)*x2*x6 + (z8^4)*x2*x7 + (z8^7 + z8^6 + z8^5)*x2*x8 + (z8^7 + z8^3 + z8 + 1)*x2*x9 + (z8^6 + z8^5 + z8^4 + z8^2 + 1)*x2*x10 + (z8^5 + z8^3 + z8^2)*x3^2 + (z8^6)*x3*x4 + (z8^4 + z8^3 + 1)*x3*x5 + (z8^7 + z8^5 + z8^4 + z8 + 1)*x3*x6 + (z8^7 + z8^6 + z8^3 + z8)*x3*x7 + (z8^4 + z8^3 + z8)*x3*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x3*x9 + (z8^4 + z8^3 + z8 + 1)*x4^2 + (z8^6 + z8^5 + z8^2)*x3*x10 + (z8^7 + z8^6 + z8^4 + z8^3 + 1)*x4^2 + (z8^6 + z8^3 + z8^2 + 1)*x4*x5 + (z8^6 + z8)*x4*x6 + (z8^7 + z8^5 + z8^3 + z8^2 + 1)*x4*x7 + (z8^6 + z8^2)*x4*x8 + (z8^6 + z8^5 + z8^4 + z8 + 1)*x4*x9 + (z8^7 + z8^5 + z8^4 + z8^3 + z8)*x4*x10 + (z8^7 + z8^4)*x5^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8)*x5*x6 + (z8^6 + z8^3 + z8^2 + z8)*x5*x7 + (z8^7 + z8^5 + z8^4)*x5*x8 + (z8^5 + z8^3 + 1)*x5*x9 + (z8^7 + z8^6)*x5*x10 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + 1)*x6^2 + (z8^7 + z8^5 + z8^2)*x6*x7 + (z8^7 + z8^4 + z8^3 + z8 + 1)*x6*x8 + (z8^4 + 1)*x6*x9 + (z8^7 + z8^2 + z8 + 1)*x6*x10 + (z8^7 + z8^5 + z8^4 + z8^2 + z8 + 1)*x7^2 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2)*x7*x8 + (z8^7 + z8^6 + z8^5 + z8^3 + z8 + 1)*x7*x9 + (z8^5 + z8^4 + z8^3 + z8^2 + z8)*x7*x10 + (z8^6 + z8^2 + z8)*x8^2 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x8*x9 + (z8^7 + z8^5 + z8^3 + z8 + 1)*x8*x10 + (z8^7 + z8^6 + z8^2 + z8 + 1)*x9^2 + (z8^5 + z8^3 + z8^2 + z8)*x10^2 + (z8)*x9*x10 + (z8^5 + z8^3 + z8^2)*x10^2,
(z8^6 + z8^5 + z8^4 + z8^2 + 1)*x0^2 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + z8)*x0*x1 + (z8^7 + z8^6 + z8^5 + z8^4 + 1)*x0*x2 + (z8^7 + z8 + 1)*x0*x3 + (z8^6 + z8^3 + 1)*x0*x4 + (z8^7 + z8^6 + z8^5 + z8^4)*x0*x5 + (z8^4 + z8^2 + 1)*x0*x6 + (z8^5 + z8^4)*x0*x7 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x8 + (z8^4 + z8^3)*x0*x9 + (z8^7 + z8)*x1^2 + (z8^5 + z8^3 + z8)*x0*x10 + (z8^6 + z8^5 + z8 + 1)*x1^2 + (z8^6 + z8^3 + z8^2 + z8 + 1)*x1*x2 + (z8^6 + z8^4 + z8^3 + 1)*x1*x3 + (z8^7 + z8^2)*x1*x4 + (z8^6 + z8^5 + z8^4 + z8^2 + z8 + 1)*x1*x5 + (z8^5 + z8^4)*x1*x6 + (z8^6 + z8^5 + z8^3)*x1*x7 + (z8^6 + z8^4 + z8)*x1*x8 + (z8^6 + z8^3 + 1)*x1*x9 + (z8^6 + z8^5 + z8^3 + z8^2 + z8)*x1*x10 + (z8^7 + z8^6 + z8^3 + z8^2)*x2^2 + (z8^2 + 1)*x2*x3 + (z8^5 + z8^3 + z8 + 1)*x2*x4 + (z8^5 + z8^4 + z8 + 1)*x2*x5 + (z8^4 + z8^3 + z8^2 + z8 + 1)*x2*x6 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + z8 + 1)*x2*x7 + (z8^5 + z8^3 + z8^2 + z8)*x2*x8 + (z8^7 + 1)*x2*x9 + (z8^5 + z8^4 + z8^2)*x2*x10 + (z8^6 + z8^3 + z8^2)*x3^2 + (z8^7 + z8^6 + z8)*x3*x4 + (z8^6 + z8^3 + z8)*x3*x5 + (z8^7 + z8^6 + z8^4 + z8^3)*x3*x6 + (z8^7 + z8^4 + z8^3 + z8 + 1)*x3*x7 + (z8^7 + z8^4 + z8^3 + z8^2 + z8 + 1)*x3*x8 + (z8^5 + z8^3 + z8^2 + z8)*x3*x9 + (z8^7 + z8^2 + z8 + 1)*x4^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8)*x3*x10 + (z8^2 + 1)*x4^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8 + 1)*x4*x5 + (z8^7 + z8^6 + z8^2)*x4*x6 + (z8^6 + z8^5 + z8^4)*x4*x7 + (z8^7 + z8^5 + z8^4 + z8^2 + z8)*x4*x8 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x4*x9 + (z8^5 + z8^4 + z8^3 + z8^2 + 1)*x4*x10 + (z8^6 + z8^4 + 1)*x5^2 + (z8^7 + z8^6 + z8^4 + z8^2 + z8 + 1)*x5*x6 + (z8^4 + z8)*x5*x7 + (z8^7 + z8^5 + z8^2 + 1)*x5*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + 1)*x5*x9 + (z8^7 + z8^5 + z8^4)*x5*x10 + (z8^6 + z8^2 + z8 + 1)*x6^2 + (z8^6 + z8^3 + z8^2 + 1)*x6*x7 + (z8^7 + z8 + 1)*x6*x8 + (z8^4 + z8^2 + z8 + 1)*x6*x9 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + z8 + 1)*x6*x10 + (z8^7 + z8^4 + z8 + 1)*x7^2 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x7*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8)*x7*x9 + (z8^7 + z8^4 + z8^3 + 1)*x7*x10 + (z8^7 + z8^6 + z8^4 + z8 + 1)*x8^2 + (z8^3 + z8 + 1)*x8*x9 + (z8^7 + z8^6 + z8^4 + z8 + 1)*x8*x10 + (z8^7 + z8^5 + 1)*x9^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x10^2 + (z8^6 + z8^3 + z8 + 1)*x9*x10 + (z8^5 + z8^2)*x10^2,
(z8^5 + z8^3 + z8^2 + 1)*x0^2 + (z8^6 + z8^5 + z8)*x0*x1 + (z8^5 + 1)*x0*x2 + (z8^6 + z8^5 + z8^4 + z8^2 + z8)*x0*x3 + (z8^6 + z8^3)*x0*x4 + (z8^5 + z8^4 + z8^3 + z8^2)*x0*x6 + (z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x7 + (z8^7 + z8^6 + z8^5 + z8^2 + 1)*x0*x8 + (z8^7 + z8^5 + z8^3 + z8 + 1)*x0*x9 + (z8^5 + z8^2 + 1)*x1^2 + (z8^7 + z8^5 + z8^3 + z8)*x0*x10 + (z8^6 + z8^5 + z8^3)*x1^2 + (z8^6 + z8^2)*x1*x2 + (z8^7 + z8^6 + z8^4 + z8)*x1*x3 + (z8^7 + z8^3 + z8^2 + 1)*x1*x4 + (z8^7 + z8^6 + z8^3 + z8 + 1)*x1*x5 + (z8^7 + z8^4 + z8^2 + z8 + 1)*x1*x6 + (z8^3 + z8^2)*x1*x7 + (z8^6)*x1*x8 + (z8^7 + z8^3 + z8^2)*x1*x9 + (z8^5 + z8^3)*x1*x10 + (z8^3 + z8^2 + 1)*x2^2 + (z8^7 + z8^5 + z8^3 + 1)*x2*x3 + (z8^6 + z8^5 + z8^3)*x2*x4 + (z8^2 + 1)*x2*x5 + (z8^7 + z8^6 + z8)*x2*x6 + (z8^5 + z8^3 + z8^2)*x2*x8 + (z8^6 + z8^3 + z8)*x2*x9 + (z8^4 + z8^3 + z8^2 + 1)*x2*x10 + (z8^7 + z8^5 + z8^3 + z8)*x3^2 + (z8^7 + z8^3)*x3*x4 + (z8^7 + z8^5 + z8^4 + 1)*x3*x5 + (z8^6 + z8^5 + z8^2 + z8)*x3*x6 + (z8^7 + z8 + 1)*x3*x7 + (z8^7 + z8^5 + z8^2)*x3*x8 + (z8^6 + z8^5 + z8^3 + z8^2)*x3*x9 + (z8^6 + z8^5 + z8^4 + z8)*x4^2 + (z8^7 + z8^6 + z8^5 + z8^2 + z8 + 1)*x3*x10 + (z8^6 + z8^4 + 1)*x4^2 + (z8^7 + z8^3 + z8^2)*x4*x5 + (z8^7 + z8^3 + z8^2 + z8)*x4*x6 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + 1)*x4*x7 + (z8^7 + z8^6 + z8^4 + z8^3 + 1)*x4*x8 + (z8^5 + z8^4 + z8^3 + z8^2 + 1)*x4*x9 + (z8^6 + z8^3 + z8^2 + z8 + 1)*x4*x10 + (z8^5 + z8^4 + z8^2 + 1)*x5^2 + (z8^5 + z8 + 1)*x5*x6 + (z8^6 + z8^2 + z8)*x5*x7 + (z8^7 + z8^5 + z8^4 + z8^2 + 1)*x5*x8 + (z8^7 + z8^4 + z8)*x5*x9 + (z8^7 + z8^6 + z8^3 + z8^2 + z8)*x5*x10 + (z8^5 + 1)*x6^2 + (z8^6 + z8^4 + z8^3 + z8^2 + z8)*x6*x7 + (z8^6 + z8^5 + z8^4 + z8^2 + z8)*x6*x8 + (z8^7 + z8^6 + z8^5 + z8^3)*x6*x9 + (z8^6 + z8^2 + z8)*x6*x10 + (z8^7 + z8^6 + z8^5)*x7^2 + (z8^5 + z8^3)*x7*x8 + (z8^6 + z8^4 + z8^2 + z8 + 1)*x7*x9 + (z8^7 + z8^5 + z8)*x7*x10 + (z8^6 + z8^4 + z8^3 + z8^2 + z8)*x8^2 + (z8^5 + z8^2 + 1)*x8*x9 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2)*x8*x10 + (z8^7 + z8^6 + z8^3 + z8^2 + z8 + 1)*x9^2 + (z8^4 + z8^3 + 1)*x10^2 + (z8^5 + z8^4 + z8^3 + z8^2 + 1)*x9*x10 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x10^2,
(z8^5 + z8^4 + z8^3 + z8)*x0^2 + (z8^6 + z8^4 + z8^3)*x0*x1 + (z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x2 + (z8^7 + z8^5 + z8^2 + z8 + 1)*x0*x3 + (z8^4 + z8^2 + 1)*x0*x4 + (z8^7 + z8^5 + z8^3 + z8^2 + z8 + 1)*x0*x5 + (z8^7 + z8^4 + z8^3 + z8 + 1)*x0*x6 + (z8^5 + z8^2 + z8)*x0*x7 + (z8^6 + z8^5 + z8 + 1)*x0*x8 + (z8^7 + z8^6 + z8^4 + 1)*x0*x9 + (z8^7 + z8^6 + z8^4 + z8^2 + z8 + 1)*x1^2 + (z8^5 + z8^4 + z8)*x0*x10 + (z8^7 + z8^5 + z8^4 + z8^3)*x1^2 + (z8^4 + z8^3)*x1*x2 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x1*x3 + (z8^4 + z8)*x1*x4 + (z8^6 + 1)*x1*x5 + (z8^7 + z8^6 + z8^4 + z8 + 1)*x1*x6 + (z8^3 + z8^2)*x1*x7 + (z8^7 + z8^5 + z8^4 + z8^2 + 1)*x1*x8 + (z8^6 + z8^2 + z8)*x1*x9 + (z8^7 + z8^5 + z8^3)*x1*x10 + (z8^7 + z8^6 + z8^2 + z8 + 1)*x2^2 + (z8^7 + z8^6 + z8^4 + z8^3 + z8 + 1)*x2*x3 + (z8^3 + z8)*x2*x4 + (z8^7 + z8^4 + z8^3 + z8 + 1)*x2*x5 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + z8)*x2*x6 + (z8^6 + z8^4 + z8^3 + z8 + 1)*x2*x7 + (z8^7 + 1)*x2*x8 + (z8^7 + z8^6 + z8^3)*x2*x9 + (z8^5 + z8^4 + z8)*x2*x10 + (z8^7 + z8^6 + z8^4 + z8^2)*x3^2 + (z8^6 + z8^5 + z8^2 + z8)*x3*x4 + (z8^6 + z8^5 + z8^4 + z8^3 + 1)*x3*x5 + (z8^6 + z8^4 + z8^3 + z8^2 + z8)*x3*x6 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x3*x7 + (z8^6 + z8^4 + z8^3 + z8)*x3*x8 + (z8^7 + z8^5 + z8^4 + z8^3 + 1)*x3*x9 + (z8^7 + z8^6 + z8^4 + z8^2 + z8 + 1)*x4^2 + (z8^4 + z8^3 + z8^2)*x3*x10 + (z8^6 + z8^5 + z8)*x4^2 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x4*x5 + (z8^4 + z8^3 + z8)*x4*x6 + (z8^6 + z8^5 + z8^3 + z8)*x4*x7 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3)*x4*x8 + (z8^5 + z8^2)*x4*x9 + (1)*x4*x10 + (z8^7 + z8^6 + z8^5)*x5^2 + (z8^7 + z8^5 + z8^3 + z8^2 + z8)*x5*x6 + (z8^6 + z8^4 + z8^2 + z8 + 1)*x5*x7 + (z8^5 + 1)*x5*x8 + (z8^6 + z8^5 + z8^4 + z8^2 + 1)*x5*x9 + (z8^6 + z8^5 + z8^2)*x5*x10 + (z8^7)*x6^2 + (z8^7 + z8^6 + z8^4 + 1)*x6*x7 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + 1)*x6*x8 + (z8^7 + z8^5 + z8^4 + z8^3 + z8 + 1)*x6*x9 + (z8^6 + z8^5 + z8^3 + z8)*x6*x10 + (z8^5 + z8^2 + z8)*x7^2 + (z8^4 + z8^2 + 1)*x7*x8 + (z8^7 + z8^6)*x7*x9 + (z8^7 + z8^3 + z8)*x7*x10 + (z8^6 + z8^4 + z8^2)*x8^2 + (z8 + 1)*x8*x9 + (z8^7 + z8^6 + z8^5 + z8^3)*x8*x10 + (z8^3 + z8 + 1)*x9^2 + (z8^7 + z8^5 + z8^2 + z8)*x10^2 + (z8^7 + z8^5 + z8^2 + z8)*x9*x10 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + z8)*x10^2,
(z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x0^2 + (z8^5)*x0*x1 + (z8^7 + z8^3 + z8^2 + z8 + 1)*x0*x2 + (z8^5 + z8 + 1)*x0*x3 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8)*x0*x4 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x0*x5 + (z8^7 + z8^6 + 1)*x0*x6 + (z8^7 + z8^3 + 1)*x0*x7 + (z8^7 + z8^6 + z8^5 + z8^3 + 1)*x0*x8 + (z8^7 + z8^5 + z8^3 + z8^2)*x0*x9 + (z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x1^2 + (z8^7 + z8^5 + z8^3 + z8^2)*x0*x10 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2)*x1^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + 1)*x1*x2 + (z8^5 + z8^4 + z8^3)*x1*x3 + (z8^4 + z8^2 + z8 + 1)*x1*x4 + (z8^7 + z8^6 + z8^3 + z8^2)*x1*x5 + (z8^7 + z8^6 + z8 + 1)*x1*x6 + (z8^4 + z8^3 + 1)*x1*x7 + (z8^7 + z8^5 + z8^2)*x1*x8 + (z8^4 + z8^2 + 1)*x1*x9 + (z8^2 + z8 + 1)*x1*x10 + (z8^5 + z8^3)*x2^2 + (z8^4 + z8^2)*x2*x3 + (z8^6 + z8^3 + z8^2 + 1)*x2*x4 + (z8^6 + z8^5 + z8^4 + z8^2 + 1)*x2*x5 + (z8^5 + z8^4 + 1)*x2*x6 + (z8^7 + z8^6 + z8^3 + z8 + 1)*x2*x7 + (z8^7 + z8^5 + z8^4 + 1)*x2*x8 + (z8^7 + z8^3 + z8)*x2*x9 + (z8^7 + z8^5 + z8^4 + z8^2)*x2*x10 + (z8^7 + z8^4 + z8^3 + z8^2 + z8)*x3^2 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + 1)*x3*x4 + (z8^7 + z8^4 + z8^3 + z8^2 + z8 + 1)*x3*x5 + (z8^6 + z8^4 + z8 + 1)*x3*x6 + (z8^6 + z8^5 + z8^4 + z8 + 1)*x3*x7 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x3*x8 + (z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x3*x9 + (z8^6 + z8^5 + z8^4 + z8^2 + z8)*x4^2 + (z8^4 + z8^2)*x3*x10 + (z8^6 + z8^4 + z8^2)*x4^2 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x4*x5 + (z8^6 + z8^5 + 1)*x4*x6 + (z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x4*x7 + (z8^7 + z8^5 + z8^3 + z8)*x4*x8 + (z8^7 + z8^6 + z8^5 + z8^2)*x4*x9 + (z8^6 + z8^4 + z8^3 + z8)*x4*x10 + (z8^7 + z8^6 + z8^4 + z8^3 + z8 + 1)*x5^2 + (z8^3 + z8 + 1)*x5*x6 + (z8^5 + z8^4 + z8^3 + z8^2)*x5*x7 + (z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x5*x8 + (z8^7 + z8^4 + z8^2 + z8)*x5*x9 + (z8^5 + z8^4 + z8^3)*x5*x10 + (z8^7 + z8^4 + z8)*x6^2 + (z8^7 + z8^4 + z8^3 + z8^2 + 1)*x6*x7 + (z8^7 + z8^5 + z8^4 + z8)*x6*x8 + (z8^5 + z8^3 + z8 + 1)*x6*x9 + (z8^7 + z8^5 + z8^2 + z8)*x6*x10 + (z8^5 + z8^3 + z8^2 + z8 + 1)*x7^2 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x7*x8 + (z8^7 + z8^6 + z8^4 + 1)*x7*x9 + (z8^6 + z8^5 + z8^3 + z8 + 1)*x7*x10 + (z8^6 + z8^5 + z8^3)*x8^2 + (z8^5 + z8^4 + z8)*x8*x9 + (z8^4 + 1)*x8*x10 + (z8^6 + z8^2)*x9^2 + (z8^7 + z8^5 + z8^3 + z8^2)*x10^2 + (z8^4 + z8^3)*x9*x10 + (z8^5 + z8^4 + z8^2)*x10^2,
(z8^7 + z8^4 + z8^2 + z8 + 1)*x0^2 + (z8^7 + z8^6 + z8^5 + z8^3 + 1)*x0*x1 + (z8^4 + z8^2 + z8 + 1)*x0*x2 + (z8^6 + z8^4 + z8^2 + z8 + 1)*x0*x3 + (z8^7 + z8^6 + z8^4 + z8^3 + z8 + 1)*x0*x4 + (z8^7 + z8^6 + z8^5 + z8^3 + z8)*x0*x5 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3)*x0*x6 + (z8^5 + z8)*x0*x7 + (z8^7 + z8^3 + z8)*x0*x8 + (z8^5 + z8^3 + z8^2 + 1)*x0*x9 + (z8^7 + z8^5 + z8^4)*x1^2 + (z8^7 + z8^6 + z8^2)*x0*x10 + (z8^7 + z8^6 + z8^2 + 1)*x1^2 + (z8^6 + z8^5 + z8^3 + z8)*x1*x2 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + z8)*x1*x3 + (z8^6 + z8^4 + 1)*x1*x4 + (z8^5 + z8^4 + z8^3 + z8)*x1*x5 + (z8^3 + z8)*x1*x6 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2)*x1*x7 + (z8^7 + z8^3 + z8^2 + z8 + 1)*x1*x8 + (z8^7 + z8^6 + z8^4 + z8^2 + z8)*x1*x9 + (z8^7 + z8^6 + z8^2 + 1)*x1*x10 + (z8^6 + z8^5 + z8^4 + z8 + 1)*x2^2 + (z8^6 + z8^5 + z8^2 + 1)*x2*x3 + (z8^5)*x2*x4 + (z8^7 + z8^2)*x2*x5 + (z8^6 + z8^3 + z8^2 + z8 + 1)*x2*x6 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + 1)*x2*x7 + (z8^5 + z8^4 + z8^3 + z8^2 + 1)*x2*x8 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8 + 1)*x2*x9 + (z8^7 + z8^5 + z8^4 + z8^3)*x2*x10 + (z8^7 + z8^4 + z8^2 + z8)*x3^2 + (z8^6 + z8^3 + z8^2 + z8)*x3*x4 + (z8^7 + z8^5 + z8)*x3*x5 + (z8^7 + z8^5 + z8^4 + z8^3 + z8)*x3*x6 + (z8^6 + z8^5 + z8^4 + z8^2)*x3*x7 + (z8^7 + z8^6 + z8^5 + z8^3 + z8)*x3*x8 + (z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x3*x9 + (z8^6 + z8^5 + z8^4 + z8^3 + 1)*x4^2 + (z8^7 + z8^5 + z8^4 + z8 + 1)*x3*x10 + (z8^7 + z8^4 + z8^2 + 1)*x4^2 + (z8^6 + z8^2 + z8)*x4*x5 + (z8^6 + z8^5 + z8^4)*x4*x6 + (z8^7 + z8^4 + z8^3 + z8^2 + 1)*x4*x7 + (z8^6 + z8^4 + z8^3 + z8 + 1)*x4*x8 + (z8^5 + z8^4)*x4*x9 + (z8^7 + z8^5 + z8^3 + z8^2 + z8 + 1)*x4*x10 + (z8^6 + z8^4 + z8^2)*x5^2 + (z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x5*x6 + (z8^7 + z8^6 + z8^3 + z8^2 + z8)*x5*x7 + (z8^7 + z8^4 + z8^3 + z8^2)*x5*x8 + (z8^7 + z8^4 + 1)*x5*x9 + (z8^7 + z8^6 + z8^5 + z8^2 + z8 + 1)*x5*x10 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x6^2 + (z8^5 + z8^4 + z8)*x6*x7 + (z8^6 + z8^5 + z8)*x6*x8 + (z8^7 + z8^6 + z8^5 + z8^3 + z8^2 + 1)*x6*x9 + (z8^7 + z8^5 + z8^2 + z8)*x6*x10 + (z8^4 + z8^3 + z8 + 1)*x7^2 + (z8^7 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x7*x8 + (z8^5 + z8^4 + z8^2 + z8 + 1)*x7*x9 + (z8^5 + z8)*x7*x10 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8)*x8^2 + (z8^5 + z8^4 + z8 + 1)*x8*x9 + (z8^7 + z8^5 + z8^4 + z8^3 + z8 + 1)*x8*x10 + (z8^6 + z8^4 + z8^3 + z8^2 + z8 + 1)*x9^2 + (z8^5 + z8^4 + z8^3 + z8 + 1)*x10^2 + (z8^7 + z8)*x9*x10 + (z8^7 + z8^6 + z8^4 + z8^3)*x10^2,
(z8^7 + z8^2 + 1)*x0^2 + (z8^7 + z8^5 + z8^3 + z8^2 + z8 + 1)*x0*x1 + (z8^7 + z8^4)*x0*x2 + (z8^5 + z8^4 + z8^3 + z8)*x0*x3 + (z8^7 + z8^3 + z8^2 + z8 + 1)*x0*x4 + (z8^7 + z8^5 + z8^3 + z8)*x0*x5 + (z8^4 + z8^3 + z8^2 + z8)*x0*x6 + (z8^7 + z8^6 + z8^2 + 1)*x0*x7 + (z8^6 + z8^5 + z8 + 1)*x0*x8 + (z8^7 + 1)*x0*x9 + (z8^6 + z8^5 + z8^4 + z8^2)*x1^2 + (z8^7 + z8^6)*x0*x10 + (z8^7 + z8^6 + z8^4 + z8^3 + z8^2 + 1)*x1^2 + (z8^7 + z8^6 + z8^3 + 1)*x1*x2 + (z8^5 + z8^3)*x1*x4 + (z8^7 + z8^6 + z8^3 + z8^2 + z8 + 1)*x1*x5 + (z8^6 + z8^4 + z8^3 + z8^2)*x1*x6 + (z8^5 + z8^3 + z8)*x1*x7 + (z8^7 + z8^5 + z8^2 + 1)*x1*x8 + (z8^7 + z8^5)*x1*x9 + (z8^7 + z8^5 + z8^3 + z8^2 + 1)*x1*x10 + (z8^7 + z8^5 + z8^4 + z8)*x2^2 + (z8^5)*x2*x3 + (z8^5 + z8^4 + z8^3 + z8^2)*x2*x4 + (z8^4 + z8^2 + 1)*x2*x5 + (z8^7 + z8^6 + z8^3 + z8)*x2*x6 + (z8^7 + z8^6)*x2*x7 + (z8^7 + z8^4 + 1)*x2*x8 + (z8^7 + z8^6 + z8^4 + z8 + 1)*x2*x9 + (z8^7 + z8^6 + z8^2 + 1)*x2*x10 + (z8^7 + z8^6 + z8^5 + z8^2 + 1)*x3^2 + (z8^5 + 1)*x3*x4 + (z8^3 + z8 + 1)*x3*x5 + (z8)*x3*x6 + (z8^6 + z8^5 + z8^3)*x3*x7 + (z8^7 + z8^5)*x3*x8 + (z8^7 + z8^6 + 1)*x3*x9 + (z8^4 + 1)*x4^2 + (z8^6 + 1)*x3*x10 + (z8^6 + z8 + 1)*x4^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8)*x4*x5 + (z8^5 + z8^4 + z8^3 + z8^2 + 1)*x4*x6 + (z8^7 + z8^6 + z8^2)*x4*x7 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^3 + z8^2 + z8 + 1)*x4*x8 + (z8^4 + z8^3 + z8^2)*x4*x9 + (z8^6 + z8^5 + z8 + 1)*x4*x10 + (z8^6 + z8^5 + z8^2)*x5^2 + (z8^4 + z8^3 + z8^2 + 1)*x5*x6 + (z8^5 + z8^4 + 1)*x5*x7 + (z8^6 + z8^4 + z8^3 + z8^2 + z8)*x5*x8 + (z8^6 + z8^4 + z8)*x5*x9 + (z8^6 + z8^5 + z8^2 + z8 + 1)*x5*x10 + (z8^6 + z8^4 + z8^2 + z8 + 1)*x6^2 + (z8^7 + z8^6 + z8^2)*x6*x7 + (z8^4 + z8^3 + z8^2 + 1)*x6*x8 + (z8^7 + z8^5 + z8^3)*x6*x9 + (z8^7 + z8^3 + z8^2)*x6*x10 + (z8^7 + z8^6 + z8^5 + z8^3 + z8 + 1)*x7^2 + (z8^7 + z8^6 + z8^5 + z8^4 + z8^2 + z8 + 1)*x7*x8 + (z8^3 + z8^2)*x7*x9 + (z8^6 + z8^5 + 1)*x7*x10 + (z8^7 + z8^3 + z8^2 + 1)*x8^2 + (z8^5 + z8^4 + z8^3 + z8)*x8*x9 + (z8^6 + z8^4 + z8^2)*x8*x10 + (z8^7 + z8^5 + z8^3 + z8^2 + 1)*x9^2 + (z8^7 + z8^5 + z8^4 + z8 + 1)*x10^2 + (z8^7 + z8^3)*x9*x10 + (z8^7 + z8^5 + 1)*x10^2]
1d22c7c2491f889d417728
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment