Instantly share code, notes, and snippets.

# hellman/1_generate_pairs.py

Last active March 26, 2019 18:27
Show Gist options
• Save hellman/45406937a064597b6b85bd10c0920cb9 to your computer and use it in GitHub Desktop.
0CTF 2019 Quals - zer0mi (Crypto 611 pts)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 #!/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()
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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_?}
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # 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) (it1[1]: return -1 elif t0[3]t1[3]: return -1 elif t0[2]t1[2]: 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], 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): 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 i1 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()
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 [(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