抱歉，您的浏览器无法访问本站
本页面需要浏览器支持（启用）JavaScript
了解详情 >

2025-西湖论剑-New-Year-Ring4-wp复现

crypto比赛

发布于：2025年2月12日

次浏览

复现参考：https://tangcuxiaojikuai.xyz/post/b73949e0.html#more

加密代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
from random import randint, choice, shuffle
from Crypto.Util.number import *
from Crypto.Cipher import AES
from hashlib import md5
from secret import flag

p = getPrime(round(20.25))
a, b, d = randint(0, p), randint(0, p), 14
A, B, seed, secret = [], [], [randint(0, p) for _ in range(4)], [randint(0, p) for _ in range(d)]

PR.<x> = PolynomialRing(GF(p))
PRq = PR.quo(PR(list(b"DASCTF_XHLJ2025")))
for i in range(ord("🚩") % sum(list(map(ord, "flag")))):
    A += [PRq.random_element().list()]
    B += [(PRq(A[i]) * PRq(secret) + PRq([choice(seed) for _ in range(d)])).list()]
    seed = [(a * _ + b) % p for _ in seed]

print("A =", [a] + A)
print("B =", ["b"]+B)
print("C =", AES.new(key=md5(str([b]+seed+secret).encode()).digest(), nonce=b"Xenny.fans.club", mode=AES.MODE_CTR).encrypt(flag).hex())

这边的话看起来像是一个rlwe类型的，但是实际观察会发现，误差向量e相比于模数p来说并不是短向量，而是随机长度，而且e的选择每一次都在改变，这也增加了造格的难度，所以这题的考点显然不是rlwe了

这边我们只能往构造等式解矩阵方程的方向靠

首先是模数p的获取，这边肯定不是硬爆的，思路就是我们可以手机题目给出的数据中系数最大的值，这个肯定是和模数p相差不了多少的，然后对她进行nextprime的枚举，本地测试的话10次以内就可以拿到模数p，对于本题来说的话是4次

得到模数p之后很明显就是收集等式了

我们知道，对商环意义下的多项式的乘法，可以转化为矩阵-向量的形式，例如我们现在有如下的等式（这边我们先忽略误差向量e，就是为了讲解关于商环下多项式到矩阵的转换）

s∗A=bs * A = b

s和A都是度为13的多项式，可以表示为

s=s0+s1∗x+s2∗x2+⋯+s13∗x13A=a0+a1∗x+a2∗x2+⋯+a13∗x13\begin{array}{l} s = s_0 + s_1 * x + s_2 * x^2 + \dots + s_{13} * x ^ {13}\\ A = a_0 + a_1 * x + a_2 * x^2 + \dots + a_{13} * x ^ {13} \end{array}

然后他们都在对应的Zp[x]/(f(x))\mathbb{Z}_p[x]/(f(x))​下，f(x)f(x)在本题的等式

53x14+50x13+48x12+50x11+74x10+76x9+72x8+88x7+95x6+70x5+84x4+67x3+83x2+65x+6853x^{14} + 50x^{13} + 48x^{12} + 50x^{11} + 74x^{10} + 76x^{9} + 72x^{8} + 88x^{7} + 95x^{6} + 70x^{5} + 84x^{4} + 67x^{3} + 83x^{2} + 65x + 68

也就是对应

1
PR(list(b"DASCTF_XHLJ2025")

那么他们相乘的结果对应的多项式也会限制他的度是13，也就是

b=b0+b1∗x+b2∗x2+⋯+b13∗x13b = b_0 + b_1 * x + b_2 * x^2 + \dots + b_{13} * x ^ {13}

转化为对应的矩阵-向量的形式

(s0,s1,…,s13)(a00a01⋯a013a10a11⋯a113⋮⋮⋱⋮a130a131⋯a1313)=(b0,b1,…,b13)\begin{array}{l} (s_0, s_1, \dots, s_{13}) \begin{pmatrix} a_{0_0} & a_{0_1} & \cdots & a_{0_{13}} \\ a_{1_0} & a_{1_1} & \cdots & a_{1_{13}} \\ \vdots & \vdots & \ddots & \vdots \\ a_{13_0} & a_{13_1} & \cdots & a_{13_{13}} \end{pmatrix}= (b_0, b_1, \dots, b_{13}) \end{array}

那么在sage中我们如何实现这个多项式A到矩阵A的转化呢，有如下的一句话代码

1
mat = Matrix(ZZ, [(mult*x^i % mod).list() for i in range(mod.degree())])

mod为对应的模多项式，本题对应就是14

mult为要转为矩阵的多项式，注意是定义在多项式环下，不是商环

具体推导实现如下：

我们知道上面的矩阵运算可以形成14组等式

对于第一组

(s0,s1,…,s13)(a00a10⋮a130)=b0\begin{array}{l} (s_0, s_1, \dots, s_{13}) \begin{pmatrix} a_{0_0} \\ a_{1_0} \\ \vdots \\ a_{13_0} \end{pmatrix}= b_0 \end{array}

对于第二组

(s0,s1,…,s13)(a01∗xa11∗x⋮a131∗x)=b1∗x\begin{array}{l} (s_0, s_1, \dots, s_{13}) \begin{pmatrix} a_{0_1} * x\\ a_{1_1} * x\\ \vdots \\ a_{13_1} *x \end{pmatrix}= b_1 * x \end{array}

以此类推

对于都限制在f(x)f(x)​​​，我们只要再模下mod就行了，让sage自己去计算

本地测试是成立的

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
from random import randint, choice, shuffle
from Crypto.Util.number import *
from Crypto.Cipher import AES
from hashlib import md5


p = getPrime(round(20.25))
a, b, d = randint(0, p), randint(0, p), 14
A, B, seed, secret = [], [], [randint(0, p) for _ in range(4)], [randint(0, p) for _ in range(d)]

PR.<x> = PolynomialRing(GF(p))
PRq = PR.quo(PR(list(b"DASCTF_XHLJ2025")))

f = PR(list(b"DASCTF_XHLJ2025"))
A = PRq.random_element()
B = PRq.random_element()

print((A * B).list())
vector(Zmod(p), A.list()) * Matrix(Zmod(p), [(PR(B.list())*x^i % f).list() for i in range(14)])

'''
[309822, 280117, 531900, 287388, 160022, 226813, 109527, 528048, 519585, 86831, 104245, 109784, 186575, 60459]
(309822, 280117, 531900, 287388, 160022, 226813, 109527, 528048, 519585, 86831, 104245, 109784, 186575, 60459)
'''

那么实现了多项式相乘到矩阵的转换之后，现在就差等式中的误差e还没解决，我们假设最初始的seed里面的四个变量分别是

(e0,e1,e2,e3)(e_0, e_1, e_2, e_3)

但是他选择误差的时候的e是随机选取的，那么这时候我们不知道他每一轮选取了哪些e，但是无论如下，我们都有如下的等式成立（对于第一组来说，这边我们开始考虑误差向量e了）

(∑i=013si∗ai0−b0+e0)∗(∑i=013si∗ai0−b0+e1)∗(∑i=013si∗ai0−b0+e2)∗(∑i=013si∗ai0−b0+e3)=0(\sum_{i=0}^{13} s_i * a_{i_0} - b_0 + e_0)* (\sum_{i=0}^{13} s_i * a_{i_0} - b_0 + e_1) * (\sum_{i=0}^{13} s_i * a_{i_0} - b_0 + e_2) * (\sum_{i=0}^{13} s_i * a_{i_0} - b_0 + e_3) = 0

每一次交互我们可以拿到14组等式，对于第二次交互的e发生了改变，我们也只要在代码中顺便进行lcg的迭代就可以了

到这部分的实现代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
from Crypto.Util.number import long_to_bytes
from gmpy2 import next_prime
from ast import literal_eval
import sys

with open('output.txt', 'r') as f:
    tmp = literal_eval(f.readline().split(' = ')[1].strip())
    a = tmp[0]
    AA = tmp[1::]
    BB = literal_eval(f.readline().split(' = ')[1].strip())[1::]
    C = f.readline().split(' = ')[1].strip()

d = 14
#先获取模数p
p = 0
for i in AA:
    if max(i) > p:
        p = max(i)
for i in BB:
    if max(i) > p:
        p = max(i)
for i in range(4):  #这边的话只要四次就可以得到p，本地测试的话十次以内就行
    p = next_prime(p)

#前面的运算只要x，只定义x运算会更快，之后拿到系数之后再用MY环来运算
PR.<x> = PolynomialRing(GF(p))
PRq = PR.quo(PR(list(b"DASCTF_XHLJ2025")))
f = PR(list(b"DASCTF_XHLJ2025"))

#这是我们自己定义的
variables = [f's{i}' for i in range(14)] + [f'e{i}' for i in range(4)] + ['b']
MY = PolynomialRing(GF(p), variables)
variables = MY.gens()
s = vector(variables[:14])
e = vector(variables[14:-1])
b = variables[-1]

polys = []
for k in range(len(AA)):
    A = Matrix(GF(p), [(PR(AA[k])*x^i % f).list() for i in range(14)])
    for i in range(14):
        eq = (s * A.column(i) + e[0] - BB[k][i]) * (s * A.column(i) + e[1] - BB[k][i]) * (s * A.column(i) + e[2] - BB[k][i]) * (s * A.column(i) + e[3] - BB[k][i])
        polys.append(eq)
    e = [a * j + b for j in e]
print(len(polys[d].monomials()))
print(len(polys[0].monomials()))
print(len(polys))

'''
8021
6561
4914
'''

这边可以看到，即使是未知项最少的时候，也远比等式4914的数量还多，我们知道解方程最重要的就是我们等式的数量要大于或者等于未知量才有可能得到该方程组的唯一解，现在显然做不到，所以我们要利用到一个取消内部置换的技巧

我们先看如下的等式

(x−e1)∗(x−e2)=0x2−e1∗x−e2∗x+e1∗e2=0\begin{array}{l} (x - e_1) * (x - e_2) = 0\\ x^2 - e_1 * x - e_2 * x + e_1 * e_2 = 0 \end{array}

可以看到我们要解的四部分的项，x2,−e1∗x,−e2∗x,e1∗e2x^2, -e_1 * x, -e_2 * x, e_1 * e_2

我们做个转换，再看如下的等式

(x−e)2=0x2−2∗e∗x+e2=0\begin{array}{l} (x - e) ^ 2 = 0\\ x^2 - 2 * e * x + e^2 = 0 \end{array}

可以看到我们只要解的三部分的项，也就是x2,−2∗e∗x,e2x^2, -2 * e * x, e^2

如果说我们只关心x的解，那么我们是不是就可以这样的内部置换来减少未知项的系数呢？

那么我们现在就把初始的未知向量(e0,e1,e2,e3)(e_0, e_1, e_2, e_3)​直接当中是一个变量e就可以了

此时的等式就变为

(∑i=013si∗ai0−b0−e)4=0(\sum_{i=0}^{13} s_i * a_{i_0} - b_0 - e) ^ 4 = 0

现在我们只要对代码做下简单的修改就可以了

另外这边还有一个要注意的点，因为第一次交互是不包含变量b的，e是最初始的e，所以前14组的项会少一些，按理说这是好的，但是因为等式数量太少了，所以这边我们到时候构建新矩阵的时候就跳过这14项，这时候虽然少了14组等式，但是等式数量也有4900个，大于未知项数4845个

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
from Crypto.Util.number import long_to_bytes
from gmpy2 import next_prime
from ast import literal_eval
import sys

with open('output.txt', 'r') as f:
    tmp = literal_eval(f.readline().split(' = ')[1].strip())
    a = tmp[0]
    AA = tmp[1::]
    BB = literal_eval(f.readline().split(' = ')[1].strip())[1::]
    C = f.readline().split(' = ')[1].strip()

d = 14
#先获取模数p
p = 0
for i in AA:
    if max(i) > p:
        p = max(i)
for i in BB:
    if max(i) > p:
        p = max(i)
for i in range(4):  #这边的话只要四次就可以得到p，本地测试的话十次以内就行
    p = next_prime(p)

#前面的运算只要x，只定义x运算会更快，之后拿到系数之后再用MY环来运算
PR.<x> = PolynomialRing(GF(p))
PRq = PR.quo(PR(list(b"DASCTF_XHLJ2025")))
f = PR(list(b"DASCTF_XHLJ2025"))

#这是我们自己定义的
variables = [f's{i}' for i in range(14)] + ['e'] + ['b']
MY = PolynomialRing(GF(p), variables)
variables = MY.gens()
s = vector(variables[:14])
e = variables[-2]
b = variables[-1]

polys = []
for k in range(len(AA)):
    A = Matrix(GF(p), [(PR(AA[k])*x^i % f).list() for i in range(14)])
    for i in range(14):
        eq = (s * A.column(i) + e - BB[k][i]) ^ 4
        polys.append(eq)
    e = a * e + b
print(len(polys))
print(len(polys[0].monomials()))
print(len(polys[d].monomials())) 
print(polys[d].monomials())

'''
4914
3876
4845
'''

每个多项式对应的项如下：

1
[s0^4, s0^3*s1, s0^2*s1^2, s0*s1^3, s1^4, s0^3*s2, s0^2*s1*s2, s0*s1^2*s2, s1^3*s2, s0^2*s2^2, s0*s1*s2^2, s1^2*s2^2, s0*s2^3, s1*s2^3, s2^4, s0^3*s3, s0^2*s1*s3, s0*s1^2*s3, s1^3*s3, s0^2*s2*s3, s0*s1*s2*s3, s1^2*s2*s3, s0*s2^2*s3, s1*s2^2*s3, s2^3*s3, s0^2*s3^2, s0*s1*s3^2, s1^2*s3^2, s0*s2*s3^2, s1*s2*s3^2, s2^2*s3^2, s0*s3^3, s1*s3^3, s2*s3^3, s3^4, s0^3*s4, s0^2*s1*s4, s0*s1^2*s4, s1^3*s4, s0^2*s2*s4, s0*s1*s2*s4, s1^2*s2*s4, s0*s2^2*s4, s1*s2^2*s4, s2^3*s4, s0^2*s3*s4, s0*s1*s3*s4, s1^2*s3*s4, s0*s2*s3*s4, s1*s2*s3*s4, s2^2*s3*s4, s0*s3^2*s4, s1*s3^2*s4, s2*s3^2*s4, s3^3*s4, s0^2*s4^2, s0*s1*s4^2, s1^2*s4^2, s0*s2*s4^2, s1*s2*s4^2, s2^2*s4^2, s0*s3*s4^2, s1*s3*s4^2, s2*s3*s4^2, s3^2*s4^2, s0*s4^3, s1*s4^3, s2*s4^3, s3*s4^3, s4^4, s0^3*s5, s0^2*s1*s5, s0*s1^2*s5, s1^3*s5, s0^2*s2*s5, s0*s1*s2*s5, s1^2*s2*s5, s0*s2^2*s5, s1*s2^2*s5, s2^3*s5, s0^2*s3*s5, s0*s1*s3*s5, s1^2*s3*s5, s0*s2*s3*s5, s1*s2*s3*s5, s2^2*s3*s5, s0*s3^2*s5, s1*s3^2*s5, s2*s3^2*s5, s3^3*s5, s0^2*s4*s5, s0*s1*s4*s5, s1^2*s4*s5, s0*s2*s4*s5, s1*s2*s4*s5, s2^2*s4*s5, s0*s3*s4*s5, s1*s3*s4*s5, s2*s3*s4*s5, s3^2*s4*s5, s0*s4^2*s5, s1*s4^2*s5, s2*s4^2*s5, s3*s4^2*s5, s4^3*s5, s0^2*s5^2, s0*s1*s5^2, s1^2*s5^2, s0*s2*s5^2, s1*s2*s5^2, s2^2*s5^2, s0*s3*s5^2, s1*s3*s5^2, s2*s3*s5^2, s3^2*s5^2, s0*s4*s5^2, s1*s4*s5^2, s2*s4*s5^2, s3*s4*s5^2, s4^2*s5^2, s0*s5^3, s1*s5^3, s2*s5^3, s3*s5^3, s4*s5^3, s5^4, s0^3*s6, s0^2*s1*s6, s0*s1^2*s6, s1^3*s6, s0^2*s2*s6, s0*s1*s2*s6, s1^2*s2*s6, s0*s2^2*s6, s1*s2^2*s6, s2^3*s6, s0^2*s3*s6, s0*s1*s3*s6, s1^2*s3*s6, s0*s2*s3*s6, s1*s2*s3*s6, s2^2*s3*s6, s0*s3^2*s6, s1*s3^2*s6, s2*s3^2*s6, s3^3*s6, s0^2*s4*s6, s0*s1*s4*s6, s1^2*s4*s6, s0*s2*s4*s6, s1*s2*s4*s6, s2^2*s4*s6, s0*s3*s4*s6, s1*s3*s4*s6, s2*s3*s4*s6, s3^2*s4*s6, s0*s4^2*s6, s1*s4^2*s6, s2*s4^2*s6, s3*s4^2*s6, s4^3*s6, s0^2*s5*s6, s0*s1*s5*s6, s1^2*s5*s6, s0*s2*s5*s6, s1*s2*s5*s6, s2^2*s5*s6, s0*s3*s5*s6, s1*s3*s5*s6, s2*s3*s5*s6, s3^2*s5*s6, s0*s4*s5*s6, s1*s4*s5*s6, s2*s4*s5*s6, s3*s4*s5*s6, s4^2*s5*s6, s0*s5^2*s6, s1*s5^2*s6, s2*s5^2*s6, s3*s5^2*s6, s4*s5^2*s6, s5^3*s6, s0^2*s6^2, s0*s1*s6^2, s1^2*s6^2, s0*s2*s6^2, s1*s2*s6^2, s2^2*s6^2, s0*s3*s6^2, s1*s3*s6^2, s2*s3*s6^2, s3^2*s6^2, s0*s4*s6^2, s1*s4*s6^2, s2*s4*s6^2, s3*s4*s6^2, s4^2*s6^2, s0*s5*s6^2, s1*s5*s6^2, s2*s5*s6^2, s3*s5*s6^2, s4*s5*s6^2, s5^2*s6^2, s0*s6^3, s1*s6^3, s2*s6^3, s3*s6^3, s4*s6^3, s5*s6^3, s6^4, s0^3*s7, s0^2*s1*s7, s0*s1^2*s7, s1^3*s7, s0^2*s2*s7, s0*s1*s2*s7, s1^2*s2*s7, s0*s2^2*s7, s1*s2^2*s7, s2^3*s7, s0^2*s3*s7, s0*s1*s3*s7, s1^2*s3*s7, s0*s2*s3*s7, s1*s2*s3*s7, s2^2*s3*s7, s0*s3^2*s7, s1*s3^2*s7, s2*s3^2*s7, s3^3*s7, s0^2*s4*s7, s0*s1*s4*s7, s1^2*s4*s7, s0*s2*s4*s7, s1*s2*s4*s7, s2^2*s4*s7, s0*s3*s4*s7, s1*s3*s4*s7, s2*s3*s4*s7, s3^2*s4*s7, s0*s4^2*s7, s1*s4^2*s7, s2*s4^2*s7, s3*s4^2*s7, s4^3*s7, s0^2*s5*s7, s0*s1*s5*s7, s1^2*s5*s7, s0*s2*s5*s7, s1*s2*s5*s7, s2^2*s5*s7, s0*s3*s5*s7, s1*s3*s5*s7, s2*s3*s5*s7, s3^2*s5*s7, s0*s4*s5*s7, s1*s4*s5*s7, s2*s4*s5*s7, s3*s4*s5*s7, s4^2*s5*s7, s0*s5^2*s7, s1*s5^2*s7, s2*s5^2*s7, s3*s5^2*s7, s4*s5^2*s7, s5^3*s7, s0^2*s6*s7, s0*s1*s6*s7, s1^2*s6*s7, s0*s2*s6*s7, s1*s2*s6*s7, s2^2*s6*s7, s0*s3*s6*s7, s1*s3*s6*s7, s2*s3*s6*s7, s3^2*s6*s7, s0*s4*s6*s7, s1*s4*s6*s7, s2*s4*s6*s7, s3*s4*s6*s7, s4^2*s6*s7, s0*s5*s6*s7, s1*s5*s6*s7, s2*s5*s6*s7, s3*s5*s6*s7, s4*s5*s6*s7, s5^2*s6*s7, s0*s6^2*s7, s1*s6^2*s7, s2*s6^2*s7, s3*s6^2*s7, s4*s6^2*s7, s5*s6^2*s7, s6^3*s7, s0^2*s7^2, s0*s1*s7^2, s1^2*s7^2, s0*s2*s7^2, s1*s2*s7^2, s2^2*s7^2, s0*s3*s7^2, s1*s3*s7^2, s2*s3*s7^2, s3^2*s7^2, s0*s4*s7^2, s1*s4*s7^2, s2*s4*s7^2, s3*s4*s7^2, s4^2*s7^2, s0*s5*s7^2, s1*s5*s7^2, s2*s5*s7^2, s3*s5*s7^2, s4*s5*s7^2, s5^2*s7^2, s0*s6*s7^2, s1*s6*s7^2, s2*s6*s7^2, s3*s6*s7^2, s4*s6*s7^2, s5*s6*s7^2, s6^2*s7^2, s0*s7^3, s1*s7^3, s2*s7^3, s3*s7^3, s4*s7^3, s5*s7^3, s6*s7^3, s7^4, s0^3*s8, s0^2*s1*s8, s0*s1^2*s8, s1^3*s8, s0^2*s2*s8, s0*s1*s2*s8, s1^2*s2*s8, s0*s2^2*s8, s1*s2^2*s8, s2^3*s8, s0^2*s3*s8, s0*s1*s3*s8, s1^2*s3*s8, s0*s2*s3*s8, s1*s2*s3*s8, s2^2*s3*s8, s0*s3^2*s8, s1*s3^2*s8, s2*s3^2*s8, s3^3*s8, s0^2*s4*s8, s0*s1*s4*s8, s1^2*s4*s8, s0*s2*s4*s8, s1*s2*s4*s8, s2^2*s4*s8, s0*s3*s4*s8, s1*s3*s4*s8, s2*s3*s4*s8, s3^2*s4*s8, s0*s4^2*s8, s1*s4^2*s8, s2*s4^2*s8, s3*s4^2*s8, s4^3*s8, s0^2*s5*s8, s0*s1*s5*s8, s1^2*s5*s8, s0*s2*s5*s8, s1*s2*s5*s8, s2^2*s5*s8, s0*s3*s5*s8, s1*s3*s5*s8, s2*s3*s5*s8, s3^2*s5*s8, s0*s4*s5*s8, s1*s4*s5*s8, s2*s4*s5*s8, s3*s4*s5*s8, s4^2*s5*s8, s0*s5^2*s8, s1*s5^2*s8, s2*s5^2*s8, s3*s5^2*s8, s4*s5^2*s8, s5^3*s8, s0^2*s6*s8, s0*s1*s6*s8, s1^2*s6*s8, s0*s2*s6*s8, s1*s2*s6*s8, s2^2*s6*s8, s0*s3*s6*s8, s1*s3*s6*s8, s2*s3*s6*s8, s3^2*s6*s8, s0*s4*s6*s8, s1*s4*s6*s8, s2*s4*s6*s8, s3*s4*s6*s8, s4^2*s6*s8, s0*s5*s6*s8, s1*s5*s6*s8, s2*s5*s6*s8, s3*s5*s6*s8, s4*s5*s6*s8, s5^2*s6*s8, s0*s6^2*s8, s1*s6^2*s8, s2*s6^2*s8, s3*s6^2*s8, s4*s6^2*s8, s5*s6^2*s8, s6^3*s8, s0^2*s7*s8, s0*s1*s7*s8, s1^2*s7*s8, s0*s2*s7*s8, s1*s2*s7*s8, s2^2*s7*s8, s0*s3*s7*s8, s1*s3*s7*s8, s2*s3*s7*s8, s3^2*s7*s8, s0*s4*s7*s8, s1*s4*s7*s8, s2*s4*s7*s8, s3*s4*s7*s8, s4^2*s7*s8, s0*s5*s7*s8, s1*s5*s7*s8, s2*s5*s7*s8, s3*s5*s7*s8, s4*s5*s7*s8, s5^2*s7*s8, s0*s6*s7*s8, s1*s6*s7*s8, s2*s6*s7*s8, s3*s6*s7*s8, s4*s6*s7*s8, s5*s6*s7*s8, s6^2*s7*s8, s0*s7^2*s8, s1*s7^2*s8, s2*s7^2*s8, s3*s7^2*s8, s4*s7^2*s8, s5*s7^2*s8, s6*s7^2*s8, s7^3*s8, s0^2*s8^2, s0*s1*s8^2, s1^2*s8^2, s0*s2*s8^2, s1*s2*s8^2, s2^2*s8^2, s0*s3*s8^2, s1*s3*s8^2, s2*s3*s8^2, s3^2*s8^2, s0*s4*s8^2, s1*s4*s8^2, s2*s4*s8^2, s3*s4*s8^2, s4^2*s8^2, s0*s5*s8^2, s1*s5*s8^2, s2*s5*s8^2, s3*s5*s8^2, s4*s5*s8^2, s5^2*s8^2, s0*s6*s8^2, s1*s6*s8^2, s2*s6*s8^2, s3*s6*s8^2, s4*s6*s8^2, s5*s6*s8^2, s6^2*s8^2, s0*s7*s8^2, s1*s7*s8^2, s2*s7*s8^2, s3*s7*s8^2, s4*s7*s8^2, s5*s7*s8^2, s6*s7*s8^2, s7^2*s8^2, s0*s8^3, s1*s8^3, s2*s8^3, s3*s8^3, s4*s8^3, s5*s8^3, s6*s8^3, s7*s8^3, s8^4, s0^3*s9, s0^2*s1*s9, s0*s1^2*s9, s1^3*s9, s0^2*s2*s9, s0*s1*s2*s9, s1^2*s2*s9, s0*s2^2*s9, s1*s2^2*s9, s2^3*s9, s0^2*s3*s9, s0*s1*s3*s9, s1^2*s3*s9, s0*s2*s3*s9, s1*s2*s3*s9, s2^2*s3*s9, s0*s3^2*s9, s1*s3^2*s9, s2*s3^2*s9, s3^3*s9, s0^2*s4*s9, s0*s1*s4*s9, s1^2*s4*s9, s0*s2*s4*s9, s1*s2*s4*s9, s2^2*s4*s9, s0*s3*s4*s9, s1*s3*s4*s9, s2*s3*s4*s9, s3^2*s4*s9, s0*s4^2*s9, s1*s4^2*s9, s2*s4^2*s9, s3*s4^2*s9, s4^3*s9, s0^2*s5*s9, s0*s1*s5*s9, s1^2*s5*s9, s0*s2*s5*s9, s1*s2*s5*s9, s2^2*s5*s9, s0*s3*s5*s9, s1*s3*s5*s9, s2*s3*s5*s9, s3^2*s5*s9, s0*s4*s5*s9, s1*s4*s5*s9, s2*s4*s5*s9, s3*s4*s5*s9, s4^2*s5*s9, s0*s5^2*s9, s1*s5^2*s9, s2*s5^2*s9, s3*s5^2*s9, s4*s5^2*s9, s5^3*s9, s0^2*s6*s9, s0*s1*s6*s9, s1^2*s6*s9, s0*s2*s6*s9, s1*s2*s6*s9, s2^2*s6*s9, s0*s3*s6*s9, s1*s3*s6*s9, s2*s3*s6*s9, s3^2*s6*s9, s0*s4*s6*s9, s1*s4*s6*s9, s2*s4*s6*s9, s3*s4*s6*s9, s4^2*s6*s9, s0*s5*s6*s9, s1*s5*s6*s9, s2*s5*s6*s9, s3*s5*s6*s9, s4*s5*s6*s9, s5^2*s6*s9, s0*s6^2*s9, s1*s6^2*s9, s2*s6^2*s9, s3*s6^2*s9, s4*s6^2*s9, s5*s6^2*s9, s6^3*s9, s0^2*s7*s9, s0*s1*s7*s9, s1^2*s7*s9, s0*s2*s7*s9, s1*s2*s7*s9, s2^2*s7*s9, s0*s3*s7*s9, s1*s3*s7*s9, s2*s3*s7*s9, s3^2*s7*s9, s0*s4*s7*s9, s1*s4*s7*s9, s2*s4*s7*s9, s3*s4*s7*s9, s4^2*s7*s9, s0*s5*s7*s9, s1*s5*s7*s9, s2*s5*s7*s9, s3*s5*s7*s9, s4*s5*s7*s9, s5^2*s7*s9, s0*s6*s7*s9, s1*s6*s7*s9, s2*s6*s7*s9, s3*s6*s7*s9, s4*s6*s7*s9, s5*s6*s7*s9, s6^2*s7*s9, s0*s7^2*s9, s1*s7^2*s9, s2*s7^2*s9, s3*s7^2*s9, s4*s7^2*s9, s5*s7^2*s9, s6*s7^2*s9, s7^3*s9, s0^2*s8*s9, s0*s1*s8*s9, s1^2*s8*s9, s0*s2*s8*s9, s1*s2*s8*s9, s2^2*s8*s9, s0*s3*s8*s9, s1*s3*s8*s9, s2*s3*s8*s9, s3^2*s8*s9, s0*s4*s8*s9, s1*s4*s8*s9, s2*s4*s8*s9, s3*s4*s8*s9, s4^2*s8*s9, s0*s5*s8*s9, s1*s5*s8*s9, s2*s5*s8*s9, s3*s5*s8*s9, s4*s5*s8*s9, s5^2*s8*s9, s0*s6*s8*s9, s1*s6*s8*s9, s2*s6*s8*s9, s3*s6*s8*s9, s4*s6*s8*s9, s5*s6*s8*s9, s6^2*s8*s9, s0*s7*s8*s9, s1*s7*s8*s9, s2*s7*s8*s9, s3*s7*s8*s9, s4*s7*s8*s9, s5*s7*s8*s9, s6*s7*s8*s9, s7^2*s8*s9, s0*s8^2*s9, s1*s8^2*s9, s2*s8^2*s9, s3*s8^2*s9, s4*s8^2*s9, s5*s8^2*s9, s6*s8^2*s9, s7*s8^2*s9, s8^3*s9, s0^2*s9^2, s0*s1*s9^2, s1^2*s9^2, s0*s2*s9^2, s1*s2*s9^2, s2^2*s9^2, s0*s3*s9^2, s1*s3*s9^2, s2*s3*s9^2, s3^2*s9^2, s0*s4*s9^2, s1*s4*s9^2, s2*s4*s9^2, s3*s4*s9^2, s4^2*s9^2, s0*s5*s9^2, s1*s5*s9^2, s2*s5*s9^2, s3*s5*s9^2, s4*s5*s9^2, s5^2*s9^2, s0*s6*s9^2, s1*s6*s9^2, s2*s6*s9^2, s3*s6*s9^2, s4*s6*s9^2, s5*s6*s9^2, s6^2*s9^2, s0*s7*s9^2, s1*s7*s9^2, s2*s7*s9^2, s3*s7*s9^2, s4*s7*s9^2, s5*s7*s9^2, s6*s7*s9^2, s7^2*s9^2, s0*s8*s9^2, s1*s8*s9^2, s2*s8*s9^2, s3*s8*s9^2, s4*s8*s9^2, s5*s8*s9^2, s6*s8*s9^2, s7*s8*s9^2, s8^2*s9^2, s0*s9^3, s1*s9^3, s2*s9^3, s3*s9^3, s4*s9^3, s5*s9^3, s6*s9^3, s7*s9^3, s8*s9^3, s9^4, s0^3*s10, s0^2*s1*s10, s0*s1^2*s10, s1^3*s10, s0^2*s2*s10, s0*s1*s2*s10, s1^2*s2*s10, s0*s2^2*s10, s1*s2^2*s10, s2^3*s10, s0^2*s3*s10, s0*s1*s3*s10, s1^2*s3*s10, s0*s2*s3*s10, s1*s2*s3*s10, s2^2*s3*s10, s0*s3^2*s10, s1*s3^2*s10, s2*s3^2*s10, s3^3*s10, s0^2*s4*s10, s0*s1*s4*s10, s1^2*s4*s10, s0*s2*s4*s10, s1*s2*s4*s10, s2^2*s4*s10, s0*s3*s4*s10, s1*s3*s4*s10, s2*s3*s4*s10, s3^2*s4*s10, s0*s4^2*s10, s1*s4^2*s10, s2*s4^2*s10, s3*s4^2*s10, s4^3*s10, s0^2*s5*s10, s0*s1*s5*s10, s1^2*s5*s10, s0*s2*s5*s10, s1*s2*s5*s10, s2^2*s5*s10, s0*s3*s5*s10, s1*s3*s5*s10, s2*s3*s5*s10, s3^2*s5*s10, s0*s4*s5*s10, s1*s4*s5*s10, s2*s4*s5*s10, s3*s4*s5*s10, s4^2*s5*s10, s0*s5^2*s10, s1*s5^2*s10, s2*s5^2*s10, s3*s5^2*s10, s4*s5^2*s10, s5^3*s10, s0^2*s6*s10, s0*s1*s6*s10, s1^2*s6*s10, s0*s2*s6*s10, s1*s2*s6*s10, s2^2*s6*s10, s0*s3*s6*s10, s1*s3*s6*s10, s2*s3*s6*s10, s3^2*s6*s10, s0*s4*s6*s10, s1*s4*s6*s10, s2*s4*s6*s10, s3*s4*s6*s10, s4^2*s6*s10, s0*s5*s6*s10, s1*s5*s6*s10, s2*s5*s6*s10, s3*s5*s6*s10, s4*s5*s6*s10, s5^2*s6*s10, s0*s6^2*s10, s1*s6^2*s10, s2*s6^2*s10, s3*s6^2*s10, s4*s6^2*s10, s5*s6^2*s10, s6^3*s10, s0^2*s7*s10, s0*s1*s7*s10, s1^2*s7*s10, s0*s2*s7*s10, s1*s2*s7*s10, s2^2*s7*s10, s0*s3*s7*s10, s1*s3*s7*s10, s2*s3*s7*s10, s3^2*s7*s10, s0*s4*s7*s10, s1*s4*s7*s10, s2*s4*s7*s10, s3*s4*s7*s10, s4^2*s7*s10, s0*s5*s7*s10, s1*s5*s7*s10, s2*s5*s7*s10, s3*s5*s7*s10, s4*s5*s7*s10, s5^2*s7*s10, s0*s6*s7*s10, s1*s6*s7*s10, s2*s6*s7*s10, s3*s6*s7*s10, s4*s6*s7*s10, s5*s6*s7*s10, s6^2*s7*s10, s0*s7^2*s10, s1*s7^2*s10, s2*s7^2*s10, s3*s7^2*s10, s4*s7^2*s10, s5*s7^2*s10, s6*s7^2*s10, s7^3*s10, s0^2*s8*s10, s0*s1*s8*s10, s1^2*s8*s10, s0*s2*s8*s10, s1*s2*s8*s10, s2^2*s8*s10, s0*s3*s8*s10, s1*s3*s8*s10, s2*s3*s8*s10, s3^2*s8*s10, s0*s4*s8*s10, s1*s4*s8*s10, s2*s4*s8*s10, s3*s4*s8*s10, s4^2*s8*s10, s0*s5*s8*s10, s1*s5*s8*s10, s2*s5*s8*s10, s3*s5*s8*s10, s4*s5*s8*s10, s5^2*s8*s10, s0*s6*s8*s10, s1*s6*s8*s10, s2*s6*s8*s10, s3*s6*s8*s10, s4*s6*s8*s10, s5*s6*s8*s10, s6^2*s8*s10, s0*s7*s8*s10, s1*s7*s8*s10, s2*s7*s8*s10, s3*s7*s8*s10, s4*s7*s8*s10, s5*s7*s8*s10, s6*s7*s8*s10, s7^2*s8*s10, s0*s8^2*s10, s1*s8^2*s10, s2*s8^2*s10, s3*s8^2*s10, s4*s8^2*s10, s5*s8^2*s10, s6*s8^2*s10, s7*s8^2*s10, s8^3*s10, s0^2*s9*s10, s0*s1*s9*s10, s1^2*s9*s10, s0*s2*s9*s10, s1*s2*s9*s10, s2^2*s9*s10, s0*s3*s9*s10, s1*s3*s9*s10, s2*s3*s9*s10, s3^2*s9*s10, s0*s4*s9*s10, s1*s4*s9*s10, s2*s4*s9*s10, s3*s4*s9*s10, s4^2*s9*s10, s0*s5*s9*s10, s1*s5*s9*s10, s2*s5*s9*s10, s3*s5*s9*s10, s4*s5*s9*s10, s5^2*s9*s10, s0*s6*s9*s10, s1*s6*s9*s10, s2*s6*s9*s10, s3*s6*s9*s10, s4*s6*s9*s10, s5*s6*s9*s10, s6^2*s9*s10, s0*s7*s9*s10, s1*s7*s9*s10, s2*s7*s9*s10, s3*s7*s9*s10, s4*s7*s9*s10, s5*s7*s9*s10, s6*s7*s9*s10, s7^2*s9*s10, s0*s8*s9*s10, s1*s8*s9*s10, s2*s8*s9*s10, s3*s8*s9*s10, s4*s8*s9*s10, s5*s8*s9*s10, s6*s8*s9*s10, s7*s8*s9*s10, s8^2*s9*s10, s0*s9^2*s10, s1*s9^2*s10, s2*s9^2*s10, s3*s9^2*s10, s4*s9^2*s10, s5*s9^2*s10, s6*s9^2*s10, s7*s9^2*s10, s8*s9^2*s10, s9^3*s10, s0^2*s10^2, s0*s1*s10^2, s1^2*s10^2, s0*s2*s10^2, s1*s2*s10^2, s2^2*s10^2, s0*s3*s10^2, s1*s3*s10^2, s2*s3*s10^2, s3^2*s10^2, s0*s4*s10^2, s1*s4*s10^2, s2*s4*s10^2, s3*s4*s10^2, s4^2*s10^2, s0*s5*s10^2, s1*s5*s10^2, s2*s5*s10^2, s3*s5*s10^2, s4*s5*s10^2, s5^2*s10^2, s0*s6*s10^2, s1*s6*s10^2, s2*s6*s10^2, s3*s6*s10^2, s4*s6*s10^2, s5*s6*s10^2, s6^2*s10^2, s0*s7*s10^2, s1*s7*s10^2, s2*s7*s10^2, s3*s7*s10^2, s4*s7*s10^2, s5*s7*s10^2, s6*s7*s10^2, s7^2*s10^2, s0*s8*s10^2, s1*s8*s10^2, s2*s8*s10^2, s3*s8*s10^2, s4*s8*s10^2, s5*s8*s10^2, s6*s8*s10^2, s7*s8*s10^2, s8^2*s10^2, s0*s9*s10^2, s1*s9*s10^2, s2*s9*s10^2, s3*s9*s10^2, s4*s9*s10^2, s5*s9*s10^2, s6*s9*s10^2, s7*s9*s10^2, s8*s9*s10^2, s9^2*s10^2, s0*s10^3, s1*s10^3, s2*s10^3, s3*s10^3, s4*s10^3, s5*s10^3, s6*s10^3, s7*s10^3, s8*s10^3, s9*s10^3, s10^4, s0^3*s11, s0^2*s1*s11, s0*s1^2*s11, s1^3*s11, s0^2*s2*s11, s0*s1*s2*s11, s1^2*s2*s11, s0*s2^2*s11, s1*s2^2*s11, s2^3*s11, s0^2*s3*s11, s0*s1*s3*s11, s1^2*s3*s11, s0*s2*s3*s11, s1*s2*s3*s11, s2^2*s3*s11, s0*s3^2*s11, s1*s3^2*s11, s2*s3^2*s11, s3^3*s11, s0^2*s4*s11, s0*s1*s4*s11, s1^2*s4*s11, s0*s2*s4*s11, s1*s2*s4*s11, s2^2*s4*s11, s0*s3*s4*s11, s1*s3*s4*s11, s2*s3*s4*s11, s3^2*s4*s11, s0*s4^2*s11, s1*s4^2*s11, s2*s4^2*s11, s3*s4^2*s11, s4^3*s11, s0^2*s5*s11, s0*s1*s5*s11, s1^2*s5*s11, s0*s2*s5*s11, s1*s2*s5*s11, s2^2*s5*s11, s0*s3*s5*s11, s1*s3*s5*s11, s2*s3*s5*s11, s3^2*s5*s11, s0*s4*s5*s11, s1*s4*s5*s11, s2*s4*s5*s11, s3*s4*s5*s11, s4^2*s5*s11, s0*s5^2*s11, s1*s5^2*s11, s2*s5^2*s11, s3*s5^2*s11, s4*s5^2*s11, s5^3*s11, s0^2*s6*s11, s0*s1*s6*s11, s1^2*s6*s11, s0*s2*s6*s11, s1*s2*s6*s11, s2^2*s6*s11, s0*s3*s6*s11, s1*s3*s6*s11, s2*s3*s6*s11, s3^2*s6*s11, s0*s4*s6*s11, s1*s4*s6*s11, s2*s4*s6*s11, s3*s4*s6*s11, s4^2*s6*s11, s0*s5*s6*s11, s1*s5*s6*s11, s2*s5*s6*s11, s3*s5*s6*s11, s4*s5*s6*s11, s5^2*s6*s11, s0*s6^2*s11, s1*s6^2*s11, s2*s6^2*s11, s3*s6^2*s11, s4*s6^2*s11, s5*s6^2*s11, s6^3*s11, s0^2*s7*s11, s0*s1*s7*s11, s1^2*s7*s11, s0*s2*s7*s11, s1*s2*s7*s11, s2^2*s7*s11, s0*s3*s7*s11, s1*s3*s7*s11, s2*s3*s7*s11, s3^2*s7*s11, s0*s4*s7*s11, s1*s4*s7*s11, s2*s4*s7*s11, s3*s4*s7*s11, s4^2*s7*s11, s0*s5*s7*s11, s1*s5*s7*s11, s2*s5*s7*s11, s3*s5*s7*s11, s4*s5*s7*s11, s5^2*s7*s11, s0*s6*s7*s11, s1*s6*s7*s11, s2*s6*s7*s11, s3*s6*s7*s11, s4*s6*s7*s11, s5*s6*s7*s11, s6^2*s7*s11, s0*s7^2*s11, s1*s7^2*s11, s2*s7^2*s11, s3*s7^2*s11, s4*s7^2*s11, s5*s7^2*s11, s6*s7^2*s11, s7^3*s11, s0^2*s8*s11, s0*s1*s8*s11, s1^2*s8*s11, s0*s2*s8*s11, s1*s2*s8*s11, s2^2*s8*s11, s0*s3*s8*s11, s1*s3*s8*s11, s2*s3*s8*s11, s3^2*s8*s11, s0*s4*s8*s11, s1*s4*s8*s11, s2*s4*s8*s11, s3*s4*s8*s11, s4^2*s8*s11, s0*s5*s8*s11, s1*s5*s8*s11, s2*s5*s8*s11, s3*s5*s8*s11, s4*s5*s8*s11, s5^2*s8*s11, s0*s6*s8*s11, s1*s6*s8*s11, s2*s6*s8*s11, s3*s6*s8*s11, s4*s6*s8*s11, s5*s6*s8*s11, s6^2*s8*s11, s0*s7*s8*s11, s1*s7*s8*s11, s2*s7*s8*s11, s3*s7*s8*s11, s4*s7*s8*s11, s5*s7*s8*s11, s6*s7*s8*s11, s7^2*s8*s11, s0*s8^2*s11, s1*s8^2*s11, s2*s8^2*s11, s3*s8^2*s11, s4*s8^2*s11, s5*s8^2*s11, s6*s8^2*s11, s7*s8^2*s11, s8^3*s11, s0^2*s9*s11, s0*s1*s9*s11, s1^2*s9*s11, s0*s2*s9*s11, s1*s2*s9*s11, s2^2*s9*s11, s0*s3*s9*s11, s1*s3*s9*s11, s2*s3*s9*s11, s3^2*s9*s11, s0*s4*s9*s11, s1*s4*s9*s11, s2*s4*s9*s11, s3*s4*s9*s11, s4^2*s9*s11, s0*s5*s9*s11, s1*s5*s9*s11, s2*s5*s9*s11, s3*s5*s9*s11, s4*s5*s9*s11, s5^2*s9*s11, s0*s6*s9*s11, s1*s6*s9*s11, s2*s6*s9*s11, s3*s6*s9*s11, s4*s6*s9*s11, s5*s6*s9*s11, s6^2*s9*s11, s0*s7*s9*s11, s1*s7*s9*s11, s2*s7*s9*s11, s3*s7*s9*s11, s4*s7*s9*s11, s5*s7*s9*s11, s6*s7*s9*s11, s7^2*s9*s11, s0*s8*s9*s11, s1*s8*s9*s11, s2*s8*s9*s11, s3*s8*s9*s11, s4*s8*s9*s11, s5*s8*s9*s11, s6*s8*s9*s11, s7*s8*s9*s11, s8^2*s9*s11, s0*s9^2*s11, s1*s9^2*s11, s2*s9^2*s11, s3*s9^2*s11, s4*s9^2*s11, s5*s9^2*s11, s6*s9^2*s11, s7*s9^2*s11, s8*s9^2*s11, s9^3*s11, s0^2*s10*s11, s0*s1*s10*s11, s1^2*s10*s11, s0*s2*s10*s11, s1*s2*s10*s11, s2^2*s10*s11, s0*s3*s10*s11, s1*s3*s10*s11, s2*s3*s10*s11, s3^2*s10*s11, s0*s4*s10*s11, s1*s4*s10*s11, s2*s4*s10*s11, s3*s4*s10*s11, s4^2*s10*s11, s0*s5*s10*s11, s1*s5*s10*s11, s2*s5*s10*s11, s3*s5*s10*s11, s4*s5*s10*s11, s5^2*s10*s11, s0*s6*s10*s11, s1*s6*s10*s11, s2*s6*s10*s11, s3*s6*s10*s11, s4*s6*s10*s11, s5*s6*s10*s11, s6^2*s10*s11, s0*s7*s10*s11, s1*s7*s10*s11, s2*s7*s10*s11, s3*s7*s10*s11, s4*s7*s10*s11, s5*s7*s10*s11, s6*s7*s10*s11, s7^2*s10*s11, s0*s8*s10*s11, s1*s8*s10*s11, s2*s8*s10*s11, s3*s8*s10*s11, s4*s8*s10*s11, s5*s8*s10*s11, s6*s8*s10*s11, s7*s8*s10*s11, s8^2*s10*s11, s0*s9*s10*s11, s1*s9*s10*s11, s2*s9*s10*s11, s3*s9*s10*s11, s4*s9*s10*s11, s5*s9*s10*s11, s6*s9*s10*s11, s7*s9*s10*s11, s8*s9*s10*s11, s9^2*s10*s11, s0*s10^2*s11, s1*s10^2*s11, s2*s10^2*s11, s3*s10^2*s11, s4*s10^2*s11, s5*s10^2*s11, s6*s10^2*s11, s7*s10^2*s11, s8*s10^2*s11, s9*s10^2*s11, s10^3*s11, s0^2*s11^2, s0*s1*s11^2, s1^2*s11^2, s0*s2*s11^2, s1*s2*s11^2, s2^2*s11^2, s0*s3*s11^2, s1*s3*s11^2, s2*s3*s11^2, s3^2*s11^2, s0*s4*s11^2, s1*s4*s11^2, s2*s4*s11^2, s3*s4*s11^2, s4^2*s11^2, s0*s5*s11^2, s1*s5*s11^2, s2*s5*s11^2, s3*s5*s11^2, s4*s5*s11^2, s5^2*s11^2, s0*s6*s11^2, s1*s6*s11^2, s2*s6*s11^2, s3*s6*s11^2, s4*s6*s11^2, s5*s6*s11^2, s6^2*s11^2, s0*s7*s11^2, s1*s7*s11^2, s2*s7*s11^2, s3*s7*s11^2, s4*s7*s11^2, s5*s7*s11^2, s6*s7*s11^2, s7^2*s11^2, s0*s8*s11^2, s1*s8*s11^2, s2*s8*s11^2, s3*s8*s11^2, s4*s8*s11^2, s5*s8*s11^2, s6*s8*s11^2, s7*s8*s11^2, s8^2*s11^2, s0*s9*s11^2, s1*s9*s11^2, s2*s9*s11^2, s3*s9*s11^2, s4*s9*s11^2, s5*s9*s11^2, s6*s9*s11^2, s7*s9*s11^2, s8*s9*s11^2, s9^2*s11^2, s0*s10*s11^2, s1*s10*s11^2, s2*s10*s11^2, s3*s10*s11^2, s4*s10*s11^2, s5*s10*s11^2, s6*s10*s11^2, s7*s10*s11^2, s8*s10*s11^2, s9*s10*s11^2, s10^2*s11^2, s0*s11^3, s1*s11^3, s2*s11^3, s3*s11^3, s4*s11^3, s5*s11^3, s6*s11^3, s7*s11^3, s8*s11^3, s9*s11^3, s10*s11^3, s11^4, s0^3*s12, s0^2*s1*s12, s0*s1^2*s12, s1^3*s12, s0^2*s2*s12, s0*s1*s2*s12, s1^2*s2*s12, s0*s2^2*s12, s1*s2^2*s12, s2^3*s12, s0^2*s3*s12, s0*s1*s3*s12, s1^2*s3*s12, s0*s2*s3*s12, s1*s2*s3*s12, s2^2*s3*s12, s0*s3^2*s12, s1*s3^2*s12, s2*s3^2*s12, s3^3*s12, s0^2*s4*s12, s0*s1*s4*s12, s1^2*s4*s12, s0*s2*s4*s12, s1*s2*s4*s12, s2^2*s4*s12, s0*s3*s4*s12, s1*s3*s4*s12, s2*s3*s4*s12, s3^2*s4*s12, s0*s4^2*s12, s1*s4^2*s12, s2*s4^2*s12, s3*s4^2*s12, s4^3*s12, s0^2*s5*s12, s0*s1*s5*s12, s1^2*s5*s12, s0*s2*s5*s12, s1*s2*s5*s12, s2^2*s5*s12, s0*s3*s5*s12, s1*s3*s5*s12, s2*s3*s5*s12, s3^2*s5*s12, s0*s4*s5*s12, s1*s4*s5*s12, s2*s4*s5*s12, s3*s4*s5*s12, s4^2*s5*s12, s0*s5^2*s12, s1*s5^2*s12, s2*s5^2*s12, s3*s5^2*s12, s4*s5^2*s12, s5^3*s12, s0^2*s6*s12, s0*s1*s6*s12, s1^2*s6*s12, s0*s2*s6*s12, s1*s2*s6*s12, s2^2*s6*s12, s0*s3*s6*s12, s1*s3*s6*s12, s2*s3*s6*s12, s3^2*s6*s12, s0*s4*s6*s12, s1*s4*s6*s12, s2*s4*s6*s12, s3*s4*s6*s12, s4^2*s6*s12, s0*s5*s6*s12, s1*s5*s6*s12, s2*s5*s6*s12, s3*s5*s6*s12, s4*s5*s6*s12, s5^2*s6*s12, s0*s6^2*s12, s1*s6^2*s12, s2*s6^2*s12, s3*s6^2*s12, s4*s6^2*s12, s5*s6^2*s12, s6^3*s12, s0^2*s7*s12, s0*s1*s7*s12, s1^2*s7*s12, s0*s2*s7*s12, s1*s2*s7*s12, s2^2*s7*s12, s0*s3*s7*s12, s1*s3*s7*s12, s2*s3*s7*s12, s3^2*s7*s12, s0*s4*s7*s12, s1*s4*s7*s12, s2*s4*s7*s12, s3*s4*s7*s12, s4^2*s7*s12, s0*s5*s7*s12, s1*s5*s7*s12, s2*s5*s7*s12, s3*s5*s7*s12, s4*s5*s7*s12, s5^2*s7*s12, s0*s6*s7*s12, s1*s6*s7*s12, s2*s6*s7*s12, s3*s6*s7*s12, s4*s6*s7*s12, s5*s6*s7*s12, s6^2*s7*s12, s0*s7^2*s12, s1*s7^2*s12, s2*s7^2*s12, s3*s7^2*s12, s4*s7^2*s12, s5*s7^2*s12, s6*s7^2*s12, s7^3*s12, s0^2*s8*s12, s0*s1*s8*s12, s1^2*s8*s12, s0*s2*s8*s12, s1*s2*s8*s12, s2^2*s8*s12, s0*s3*s8*s12, s1*s3*s8*s12, s2*s3*s8*s12, s3^2*s8*s12, s0*s4*s8*s12, s1*s4*s8*s12, s2*s4*s8*s12, s3*s4*s8*s12, s4^2*s8*s12, s0*s5*s8*s12, s1*s5*s8*s12, s2*s5*s8*s12, s3*s5*s8*s12, s4*s5*s8*s12, s5^2*s8*s12, s0*s6*s8*s12, s1*s6*s8*s12, s2*s6*s8*s12, s3*s6*s8*s12, s4*s6*s8*s12, s5*s6*s8*s12, s6^2*s8*s12, s0*s7*s8*s12, s1*s7*s8*s12, s2*s7*s8*s12, s3*s7*s8*s12, s4*s7*s8*s12, s5*s7*s8*s12, s6*s7*s8*s12, s7^2*s8*s12, s0*s8^2*s12, s1*s8^2*s12, s2*s8^2*s12, s3*s8^2*s12, s4*s8^2*s12, s5*s8^2*s12, s6*s8^2*s12, s7*s8^2*s12, s8^3*s12, s0^2*s9*s12, s0*s1*s9*s12, s1^2*s9*s12, s0*s2*s9*s12, s1*s2*s9*s12, s2^2*s9*s12, s0*s3*s9*s12, s1*s3*s9*s12, s2*s3*s9*s12, s3^2*s9*s12, s0*s4*s9*s12, s1*s4*s9*s12, s2*s4*s9*s12, s3*s4*s9*s12, s4^2*s9*s12, s0*s5*s9*s12, s1*s5*s9*s12, s2*s5*s9*s12, s3*s5*s9*s12, s4*s5*s9*s12, s5^2*s9*s12, s0*s6*s9*s12, s1*s6*s9*s12, s2*s6*s9*s12, s3*s6*s9*s12, s4*s6*s9*s12, s5*s6*s9*s12, s6^2*s9*s12, s0*s7*s9*s12, s1*s7*s9*s12, s2*s7*s9*s12, s3*s7*s9*s12, s4*s7*s9*s12, s5*s7*s9*s12, s6*s7*s9*s12, s7^2*s9*s12, s0*s8*s9*s12, s1*s8*s9*s12, s2*s8*s9*s12, s3*s8*s9*s12, s4*s8*s9*s12, s5*s8*s9*s12, s6*s8*s9*s12, s7*s8*s9*s12, s8^2*s9*s12, s0*s9^2*s12, s1*s9^2*s12, s2*s9^2*s12, s3*s9^2*s12, s4*s9^2*s12, s5*s9^2*s12, s6*s9^2*s12, s7*s9^2*s12, s8*s9^2*s12, s9^3*s12, s0^2*s10*s12, s0*s1*s10*s12, s1^2*s10*s12, s0*s2*s10*s12, s1*s2*s10*s12, s2^2*s10*s12, s0*s3*s10*s12, s1*s3*s10*s12, s2*s3*s10*s12, s3^2*s10*s12, s0*s4*s10*s12, s1*s4*s10*s12, s2*s4*s10*s12, s3*s4*s10*s12, s4^2*s10*s12, s0*s5*s10*s12, s1*s5*s10*s12, s2*s5*s10*s12, s3*s5*s10*s12, s4*s5*s10*s12, s5^2*s10*s12, s0*s6*s10*s12, s1*s6*s10*s12, s2*s6*s10*s12, s3*s6*s10*s12, s4*s6*s10*s12, s5*s6*s10*s12, s6^2*s10*s12, s0*s7*s10*s12, s1*s7*s10*s12, s2*s7*s10*s12, s3*s7*s10*s12, s4*s7*s10*s12, s5*s7*s10*s12, s6*s7*s10*s12, s7^2*s10*s12, s0*s8*s10*s12, s1*s8*s10*s12, s2*s8*s10*s12, s3*s8*s10*s12, s4*s8*s10*s12, s5*s8*s10*s12, s6*s8*s10*s12, s7*s8*s10*s12, s8^2*s10*s12, s0*s9*s10*s12, s1*s9*s10*s12, s2*s9*s10*s12, s3*s9*s10*s12, s4*s9*s10*s12, s5*s9*s10*s12, s6*s9*s10*s12, s7*s9*s10*s12, s8*s9*s10*s12, s9^2*s10*s12, s0*s10^2*s12, s1*s10^2*s12, s2*s10^2*s12, s3*s10^2*s12, s4*s10^2*s12, s5*s10^2*s12, s6*s10^2*s12, s7*s10^2*s12, s8*s10^2*s12, s9*s10^2*s12, s10^3*s12, s0^2*s11*s12, s0*s1*s11*s12, s1^2*s11*s12, s0*s2*s11*s12, s1*s2*s11*s12, s2^2*s11*s12, s0*s3*s11*s12, s1*s3*s11*s12, s2*s3*s11*s12, s3^2*s11*s12, s0*s4*s11*s12, s1*s4*s11*s12, s2*s4*s11*s12, s3*s4*s11*s12, s4^2*s11*s12, s0*s5*s11*s12, s1*s5*s11*s12, s2*s5*s11*s12, s3*s5*s11*s12, s4*s5*s11*s12, s5^2*s11*s12, s0*s6*s11*s12, s1*s6*s11*s12, s2*s6*s11*s12, s3*s6*s11*s12, s4*s6*s11*s12, s5*s6*s11*s12, s6^2*s11*s12, s0*s7*s11*s12, s1*s7*s11*s12, s2*s7*s11*s12, s3*s7*s11*s12, s4*s7*s11*s12, s5*s7*s11*s12, s6*s7*s11*s12, s7^2*s11*s12, s0*s8*s11*s12, s1*s8*s11*s12, s2*s8*s11*s12, s3*s8*s11*s12, s4*s8*s11*s12, s5*s8*s11*s12, s6*s8*s11*s12, s7*s8*s11*s12, s8^2*s11*s12, s0*s9*s11*s12, s1*s9*s11*s12, s2*s9*s11*s12, s3*s9*s11*s12, s4*s9*s11*s12, s5*s9*s11*s12, s6*s9*s11*s12, s7*s9*s11*s12, s8*s9*s11*s12, s9^2*s11*s12, s0*s10*s11*s12, s1*s10*s11*s12, s2*s10*s11*s12, s3*s10*s11*s12, s4*s10*s11*s12, s5*s10*s11*s12, s6*s10*s11*s12, s7*s10*s11*s12, s8*s10*s11*s12, s9*s10*s11*s12, s10^2*s11*s12, s0*s11^2*s12, s1*s11^2*s12, s2*s11^2*s12, s3*s11^2*s12, s4*s11^2*s12, s5*s11^2*s12, s6*s11^2*s12, s7*s11^2*s12, s8*s11^2*s12, s9*s11^2*s12, s10*s11^2*s12, s11^3*s12, s0^2*s12^2, s0*s1*s12^2, s1^2*s12^2, s0*s2*s12^2, s1*s2*s12^2, s2^2*s12^2, s0*s3*s12^2, s1*s3*s12^2, s2*s3*s12^2, s3^2*s12^2, s0*s4*s12^2, s1*s4*s12^2, s2*s4*s12^2, s3*s4*s12^2, s4^2*s12^2, s0*s5*s12^2, s1*s5*s12^2, s2*s5*s12^2, s3*s5*s12^2, s4*s5*s12^2, s5^2*s12^2, s0*s6*s12^2, s1*s6*s12^2, s2*s6*s12^2, s3*s6*s12^2, s4*s6*s12^2, s5*s6*s12^2, s6^2*s12^2, s0*s7*s12^2, s1*s7*s12^2, s2*s7*s12^2, s3*s7*s12^2, s4*s7*s12^2, s5*s7*s12^2, s6*s7*s12^2, s7^2*s12^2, s0*s8*s12^2, s1*s8*s12^2, s2*s8*s12^2, s3*s8*s12^2, s4*s8*s12^2, s5*s8*s12^2, s6*s8*s12^2, s7*s8*s12^2, s8^2*s12^2, s0*s9*s12^2, s1*s9*s12^2, s2*s9*s12^2, s3*s9*s12^2, s4*s9*s12^2, s5*s9*s12^2, s6*s9*s12^2, s7*s9*s12^2, s8*s9*s12^2, s9^2*s12^2, s0*s10*s12^2, s1*s10*s12^2, s2*s10*s12^2, s3*s10*s12^2, s4*s10*s12^2, s5*s10*s12^2, s6*s10*s12^2, s7*s10*s12^2, s8*s10*s12^2, s9*s10*s12^2, s10^2*s12^2, s0*s11*s12^2, s1*s11*s12^2, s2*s11*s12^2, s3*s11*s12^2, s4*s11*s12^2, s5*s11*s12^2, s6*s11*s12^2, s7*s11*s12^2, s8*s11*s12^2, s9*s11*s12^2, s10*s11*s12^2, s11^2*s12^2, s0*s12^3, s1*s12^3, s2*s12^3, s3*s12^3, s4*s12^3, s5*s12^3, s6*s12^3, s7*s12^3, s8*s12^3, s9*s12^3, s10*s12^3, s11*s12^3, s12^4, s0^3*s13, s0^2*s1*s13, s0*s1^2*s13, s1^3*s13, s0^2*s2*s13, s0*s1*s2*s13, s1^2*s2*s13, s0*s2^2*s13, s1*s2^2*s13, s2^3*s13, s0^2*s3*s13, s0*s1*s3*s13, s1^2*s3*s13, s0*s2*s3*s13, s1*s2*s3*s13, s2^2*s3*s13, s0*s3^2*s13, s1*s3^2*s13, s2*s3^2*s13, s3^3*s13, s0^2*s4*s13, s0*s1*s4*s13, s1^2*s4*s13, s0*s2*s4*s13, s1*s2*s4*s13, s2^2*s4*s13, s0*s3*s4*s13, s1*s3*s4*s13, s2*s3*s4*s13, s3^2*s4*s13, s0*s4^2*s13, s1*s4^2*s13, s2*s4^2*s13, s3*s4^2*s13, s4^3*s13, s0^2*s5*s13, s0*s1*s5*s13, s1^2*s5*s13, s0*s2*s5*s13, s1*s2*s5*s13, s2^2*s5*s13, s0*s3*s5*s13, s1*s3*s5*s13, s2*s3*s5*s13, s3^2*s5*s13, s0*s4*s5*s13, s1*s4*s5*s13, s2*s4*s5*s13, s3*s4*s5*s13, s4^2*s5*s13, s0*s5^2*s13, s1*s5^2*s13, s2*s5^2*s13, s3*s5^2*s13, s4*s5^2*s13, s5^3*s13, s0^2*s6*s13, s0*s1*s6*s13, s1^2*s6*s13, s0*s2*s6*s13, s1*s2*s6*s13, s2^2*s6*s13, s0*s3*s6*s13, s1*s3*s6*s13, s2*s3*s6*s13, s3^2*s6*s13, s0*s4*s6*s13, s1*s4*s6*s13, s2*s4*s6*s13, s3*s4*s6*s13, s4^2*s6*s13, s0*s5*s6*s13, s1*s5*s6*s13, s2*s5*s6*s13, s3*s5*s6*s13, s4*s5*s6*s13, s5^2*s6*s13, s0*s6^2*s13, s1*s6^2*s13, s2*s6^2*s13, s3*s6^2*s13, s4*s6^2*s13, s5*s6^2*s13, s6^3*s13, s0^2*s7*s13, s0*s1*s7*s13, s1^2*s7*s13, s0*s2*s7*s13, s1*s2*s7*s13, s2^2*s7*s13, s0*s3*s7*s13, s1*s3*s7*s13, s2*s3*s7*s13, s3^2*s7*s13, s0*s4*s7*s13, s1*s4*s7*s13, s2*s4*s7*s13, s3*s4*s7*s13, s4^2*s7*s13, s0*s5*s7*s13, s1*s5*s7*s13, s2*s5*s7*s13, s3*s5*s7*s13, s4*s5*s7*s13, s5^2*s7*s13, s0*s6*s7*s13, s1*s6*s7*s13, s2*s6*s7*s13, s3*s6*s7*s13, s4*s6*s7*s13, s5*s6*s7*s13, s6^2*s7*s13, s0*s7^2*s13, s1*s7^2*s13, s2*s7^2*s13, s3*s7^2*s13, s4*s7^2*s13, s5*s7^2*s13, s6*s7^2*s13, s7^3*s13, s0^2*s8*s13, s0*s1*s8*s13, s1^2*s8*s13, s0*s2*s8*s13, s1*s2*s8*s13, s2^2*s8*s13, s0*s3*s8*s13, s1*s3*s8*s13, s2*s3*s8*s13, s3^2*s8*s13, s0*s4*s8*s13, s1*s4*s8*s13, s2*s4*s8*s13, s3*s4*s8*s13, s4^2*s8*s13, s0*s5*s8*s13, s1*s5*s8*s13, s2*s5*s8*s13, s3*s5*s8*s13, s4*s5*s8*s13, s5^2*s8*s13, s0*s6*s8*s13, s1*s6*s8*s13, s2*s6*s8*s13, s3*s6*s8*s13, s4*s6*s8*s13, s5*s6*s8*s13, s6^2*s8*s13, s0*s7*s8*s13, s1*s7*s8*s13, s2*s7*s8*s13, s3*s7*s8*s13, s4*s7*s8*s13, s5*s7*s8*s13, s6*s7*s8*s13, s7^2*s8*s13, s0*s8^2*s13, s1*s8^2*s13, s2*s8^2*s13, s3*s8^2*s13, s4*s8^2*s13, s5*s8^2*s13, s6*s8^2*s13, s7*s8^2*s13, s8^3*s13, s0^2*s9*s13, s0*s1*s9*s13, s1^2*s9*s13, s0*s2*s9*s13, s1*s2*s9*s13, s2^2*s9*s13, s0*s3*s9*s13, s1*s3*s9*s13, s2*s3*s9*s13, s3^2*s9*s13, s0*s4*s9*s13, s1*s4*s9*s13, s2*s4*s9*s13, s3*s4*s9*s13, s4^2*s9*s13, s0*s5*s9*s13, s1*s5*s9*s13, s2*s5*s9*s13, s3*s5*s9*s13, s4*s5*s9*s13, s5^2*s9*s13, s0*s6*s9*s13, s1*s6*s9*s13, s2*s6*s9*s13, s3*s6*s9*s13, s4*s6*s9*s13, s5*s6*s9*s13, s6^2*s9*s13, s0*s7*s9*s13, s1*s7*s9*s13, s2*s7*s9*s13, s3*s7*s9*s13, s4*s7*s9*s13, s5*s7*s9*s13, s6*s7*s9*s13, s7^2*s9*s13, s0*s8*s9*s13, s1*s8*s9*s13, s2*s8*s9*s13, s3*s8*s9*s13, s4*s8*s9*s13, s5*s8*s9*s13, s6*s8*s9*s13, s7*s8*s9*s13, s8^2*s9*s13, s0*s9^2*s13, s1*s9^2*s13, s2*s9^2*s13, s3*s9^2*s13, s4*s9^2*s13, s5*s9^2*s13, s6*s9^2*s13, s7*s9^2*s13, s8*s9^2*s13, s9^3*s13, s0^2*s10*s13, s0*s1*s10*s13, s1^2*s10*s13, s0*s2*s10*s13, s1*s2*s10*s13, s2^2*s10*s13, s0*s3*s10*s13, s1*s3*s10*s13, s2*s3*s10*s13, s3^2*s10*s13, s0*s4*s10*s13, s1*s4*s10*s13, s2*s4*s10*s13, s3*s4*s10*s13, s4^2*s10*s13, s0*s5*s10*s13, s1*s5*s10*s13, s2*s5*s10*s13, s3*s5*s10*s13, s4*s5*s10*s13, s5^2*s10*s13, s0*s6*s10*s13, s1*s6*s10*s13, s2*s6*s10*s13, s3*s6*s10*s13, s4*s6*s10*s13, s5*s6*s10*s13, s6^2*s10*s13, s0*s7*s10*s13, s1*s7*s10*s13, s2*s7*s10*s13, s3*s7*s10*s13, s4*s7*s10*s13, s5*s7*s10*s13, s6*s7*s10*s13, s7^2*s10*s13, s0*s8*s10*s13, s1*s8*s10*s13, s2*s8*s10*s13, s3*s8*s10*s13, s4*s8*s10*s13, s5*s8*s10*s13, s6*s8*s10*s13, s7*s8*s10*s13, s8^2*s10*s13, s0*s9*s10*s13, s1*s9*s10*s13, s2*s9*s10*s13, s3*s9*s10*s13, s4*s9*s10*s13, s5*s9*s10*s13, s6*s9*s10*s13, s7*s9*s10*s13, s8*s9*s10*s13, s9^2*s10*s13, s0*s10^2*s13, s1*s10^2*s13, s2*s10^2*s13, s3*s10^2*s13, s4*s10^2*s13, s5*s10^2*s13, s6*s10^2*s13, s7*s10^2*s13, s8*s10^2*s13, s9*s10^2*s13, s10^3*s13, s0^2*s11*s13, s0*s1*s11*s13, s1^2*s11*s13, s0*s2*s11*s13, s1*s2*s11*s13, s2^2*s11*s13, s0*s3*s11*s13, s1*s3*s11*s13, s2*s3*s11*s13, s3^2*s11*s13, s0*s4*s11*s13, s1*s4*s11*s13, s2*s4*s11*s13, s3*s4*s11*s13, s4^2*s11*s13, s0*s5*s11*s13, s1*s5*s11*s13, s2*s5*s11*s13, s3*s5*s11*s13, s4*s5*s11*s13, s5^2*s11*s13, s0*s6*s11*s13, s1*s6*s11*s13, s2*s6*s11*s13, s3*s6*s11*s13, s4*s6*s11*s13, s5*s6*s11*s13, s6^2*s11*s13, s0*s7*s11*s13, s1*s7*s11*s13, s2*s7*s11*s13, s3*s7*s11*s13, s4*s7*s11*s13, s5*s7*s11*s13, s6*s7*s11*s13, s7^2*s11*s13, s0*s8*s11*s13, s1*s8*s11*s13, s2*s8*s11*s13, s3*s8*s11*s13, s4*s8*s11*s13, s5*s8*s11*s13, s6*s8*s11*s13, s7*s8*s11*s13, s8^2*s11*s13, s0*s9*s11*s13, s1*s9*s11*s13, s2*s9*s11*s13, s3*s9*s11*s13, s4*s9*s11*s13, s5*s9*s11*s13, s6*s9*s11*s13, s7*s9*s11*s13, s8*s9*s11*s13, s9^2*s11*s13, s0*s10*s11*s13, s1*s10*s11*s13, s2*s10*s11*s13, s3*s10*s11*s13, s4*s10*s11*s13, s5*s10*s11*s13, s6*s10*s11*s13, s7*s10*s11*s13, s8*s10*s11*s13, s9*s10*s11*s13, s10^2*s11*s13, s0*s11^2*s13, s1*s11^2*s13, s2*s11^2*s13, s3*s11^2*s13, s4*s11^2*s13, s5*s11^2*s13, s6*s11^2*s13, s7*s11^2*s13, s8*s11^2*s13, s9*s11^2*s13, s10*s11^2*s13, s11^3*s13, s0^2*s12*s13, s0*s1*s12*s13, s1^2*s12*s13, s0*s2*s12*s13, s1*s2*s12*s13, s2^2*s12*s13, s0*s3*s12*s13, s1*s3*s12*s13, s2*s3*s12*s13, s3^2*s12*s13, s0*s4*s12*s13, s1*s4*s12*s13, s2*s4*s12*s13, s3*s4*s12*s13, s4^2*s12*s13, s0*s5*s12*s13, s1*s5*s12*s13, s2*s5*s12*s13, s3*s5*s12*s13, s4*s5*s12*s13, s5^2*s12*s13, s0*s6*s12*s13, s1*s6*s12*s13, s2*s6*s12*s13, s3*s6*s12*s13, s4*s6*s12*s13, s5*s6*s12*s13, s6^2*s12*s13, s0*s7*s12*s13, s1*s7*s12*s13, s2*s7*s12*s13, s3*s7*s12*s13, s4*s7*s12*s13, s5*s7*s12*s13, s6*s7*s12*s13, s7^2*s12*s13, s0*s8*s12*s13, s1*s8*s12*s13, s2*s8*s12*s13, s3*s8*s12*s13, s4*s8*s12*s13, s5*s8*s12*s13, s6*s8*s12*s13, s7*s8*s12*s13, s8^2*s12*s13, s0*s9*s12*s13, s1*s9*s12*s13, s2*s9*s12*s13, s3*s9*s12*s13, s4*s9*s12*s13, s5*s9*s12*s13, s6*s9*s12*s13, s7*s9*s12*s13, s8*s9*s12*s13, s9^2*s12*s13, s0*s10*s12*s13, s1*s10*s12*s13, s2*s10*s12*s13, s3*s10*s12*s13, s4*s10*s12*s13, s5*s10*s12*s13, s6*s10*s12*s13, s7*s10*s12*s13, s8*s10*s12*s13, s9*s10*s12*s13, s10^2*s12*s13, s0*s11*s12*s13, s1*s11*s12*s13, s2*s11*s12*s13, s3*s11*s12*s13, s4*s11*s12*s13, s5*s11*s12*s13, s6*s11*s12*s13, s7*s11*s12*s13, s8*s11*s12*s13, s9*s11*s12*s13, s10*s11*s12*s13, s11^2*s12*s13, s0*s12^2*s13, s1*s12^2*s13, s2*s12^2*s13, s3*s12^2*s13, s4*s12^2*s13, s5*s12^2*s13, s6*s12^2*s13, s7*s12^2*s13, s8*s12^2*s13, s9*s12^2*s13, s10*s12^2*s13, s11*s12^2*s13, s12^3*s13, s0^2*s13^2, s0*s1*s13^2, s1^2*s13^2, s0*s2*s13^2, s1*s2*s13^2, s2^2*s13^2, s0*s3*s13^2, s1*s3*s13^2, s2*s3*s13^2, s3^2*s13^2, s0*s4*s13^2, s1*s4*s13^2, s2*s4*s13^2, s3*s4*s13^2, s4^2*s13^2, s0*s5*s13^2, s1*s5*s13^2, s2*s5*s13^2, s3*s5*s13^2, s4*s5*s13^2, s5^2*s13^2, s0*s6*s13^2, s1*s6*s13^2, s2*s6*s13^2, s3*s6*s13^2, s4*s6*s13^2, s5*s6*s13^2, s6^2*s13^2, s0*s7*s13^2, s1*s7*s13^2, s2*s7*s13^2, s3*s7*s13^2, s4*s7*s13^2, s5*s7*s13^2, s6*s7*s13^2, s7^2*s13^2, s0*s8*s13^2, s1*s8*s13^2, s2*s8*s13^2, s3*s8*s13^2, s4*s8*s13^2, s5*s8*s13^2, s6*s8*s13^2, s7*s8*s13^2, s8^2*s13^2, s0*s9*s13^2, s1*s9*s13^2, s2*s9*s13^2, s3*s9*s13^2, s4*s9*s13^2, s5*s9*s13^2, s6*s9*s13^2, s7*s9*s13^2, s8*s9*s13^2, s9^2*s13^2, s0*s10*s13^2, s1*s10*s13^2, s2*s10*s13^2, s3*s10*s13^2, s4*s10*s13^2, s5*s10*s13^2, s6*s10*s13^2, s7*s10*s13^2, s8*s10*s13^2, s9*s10*s13^2, s10^2*s13^2, s0*s11*s13^2, s1*s11*s13^2, s2*s11*s13^2, s3*s11*s13^2, s4*s11*s13^2, s5*s11*s13^2, s6*s11*s13^2, s7*s11*s13^2, s8*s11*s13^2, s9*s11*s13^2, s10*s11*s13^2, s11^2*s13^2, s0*s12*s13^2, s1*s12*s13^2, s2*s12*s13^2, s3*s12*s13^2, s4*s12*s13^2, s5*s12*s13^2, s6*s12*s13^2, s7*s12*s13^2, s8*s12*s13^2, s9*s12*s13^2, s10*s12*s13^2, s11*s12*s13^2, s12^2*s13^2, s0*s13^3, s1*s13^3, s2*s13^3, s3*s13^3, s4*s13^3, s5*s13^3, s6*s13^3, s7*s13^3, s8*s13^3, s9*s13^3, s10*s13^3, s11*s13^3, s12*s13^3, s13^4, s0^3*e, s0^2*s1*e, s0*s1^2*e, s1^3*e, s0^2*s2*e, s0*s1*s2*e, s1^2*s2*e, s0*s2^2*e, s1*s2^2*e, s2^3*e, s0^2*s3*e, s0*s1*s3*e, s1^2*s3*e, s0*s2*s3*e, s1*s2*s3*e, s2^2*s3*e, s0*s3^2*e, s1*s3^2*e, s2*s3^2*e, s3^3*e, s0^2*s4*e, s0*s1*s4*e, s1^2*s4*e, s0*s2*s4*e, s1*s2*s4*e, s2^2*s4*e, s0*s3*s4*e, s1*s3*s4*e, s2*s3*s4*e, s3^2*s4*e, s0*s4^2*e, s1*s4^2*e, s2*s4^2*e, s3*s4^2*e, s4^3*e, s0^2*s5*e, s0*s1*s5*e, s1^2*s5*e, s0*s2*s5*e, s1*s2*s5*e, s2^2*s5*e, s0*s3*s5*e, s1*s3*s5*e, s2*s3*s5*e, s3^2*s5*e, s0*s4*s5*e, s1*s4*s5*e, s2*s4*s5*e, s3*s4*s5*e, s4^2*s5*e, s0*s5^2*e, s1*s5^2*e, s2*s5^2*e, s3*s5^2*e, s4*s5^2*e, s5^3*e, s0^2*s6*e, s0*s1*s6*e, s1^2*s6*e, s0*s2*s6*e, s1*s2*s6*e, s2^2*s6*e, s0*s3*s6*e, s1*s3*s6*e, s2*s3*s6*e, s3^2*s6*e, s0*s4*s6*e, s1*s4*s6*e, s2*s4*s6*e, s3*s4*s6*e, s4^2*s6*e, s0*s5*s6*e, s1*s5*s6*e, s2*s5*s6*e, s3*s5*s6*e, s4*s5*s6*e, s5^2*s6*e, s0*s6^2*e, s1*s6^2*e, s2*s6^2*e, s3*s6^2*e, s4*s6^2*e, s5*s6^2*e, s6^3*e, s0^2*s7*e, s0*s1*s7*e, s1^2*s7*e, s0*s2*s7*e, s1*s2*s7*e, s2^2*s7*e, s0*s3*s7*e, s1*s3*s7*e, s2*s3*s7*e, s3^2*s7*e, s0*s4*s7*e, s1*s4*s7*e, s2*s4*s7*e, s3*s4*s7*e, s4^2*s7*e, s0*s5*s7*e, s1*s5*s7*e, s2*s5*s7*e, s3*s5*s7*e, s4*s5*s7*e, s5^2*s7*e, s0*s6*s7*e, s1*s6*s7*e, s2*s6*s7*e, s3*s6*s7*e, s4*s6*s7*e, s5*s6*s7*e, s6^2*s7*e, s0*s7^2*e, s1*s7^2*e, s2*s7^2*e, s3*s7^2*e, s4*s7^2*e, s5*s7^2*e, s6*s7^2*e, s7^3*e, s0^2*s8*e, s0*s1*s8*e, s1^2*s8*e, s0*s2*s8*e, s1*s2*s8*e, s2^2*s8*e, s0*s3*s8*e, s1*s3*s8*e, s2*s3*s8*e, s3^2*s8*e, s0*s4*s8*e, s1*s4*s8*e, s2*s4*s8*e, s3*s4*s8*e, s4^2*s8*e, s0*s5*s8*e, s1*s5*s8*e, s2*s5*s8*e, s3*s5*s8*e, s4*s5*s8*e, s5^2*s8*e, s0*s6*s8*e, s1*s6*s8*e, s2*s6*s8*e, s3*s6*s8*e, s4*s6*s8*e, s5*s6*s8*e, s6^2*s8*e, s0*s7*s8*e, s1*s7*s8*e, s2*s7*s8*e, s3*s7*s8*e, s4*s7*s8*e, s5*s7*s8*e, s6*s7*s8*e, s7^2*s8*e, s0*s8^2*e, s1*s8^2*e, s2*s8^2*e, s3*s8^2*e, s4*s8^2*e, s5*s8^2*e, s6*s8^2*e, s7*s8^2*e, s8^3*e, s0^2*s9*e, s0*s1*s9*e, s1^2*s9*e, s0*s2*s9*e, s1*s2*s9*e, s2^2*s9*e, s0*s3*s9*e, s1*s3*s9*e, s2*s3*s9*e, s3^2*s9*e, s0*s4*s9*e, s1*s4*s9*e, s2*s4*s9*e, s3*s4*s9*e, s4^2*s9*e, s0*s5*s9*e, s1*s5*s9*e, s2*s5*s9*e, s3*s5*s9*e, s4*s5*s9*e, s5^2*s9*e, s0*s6*s9*e, s1*s6*s9*e, s2*s6*s9*e, s3*s6*s9*e, s4*s6*s9*e, s5*s6*s9*e, s6^2*s9*e, s0*s7*s9*e, s1*s7*s9*e, s2*s7*s9*e, s3*s7*s9*e, s4*s7*s9*e, s5*s7*s9*e, s6*s7*s9*e, s7^2*s9*e, s0*s8*s9*e, s1*s8*s9*e, s2*s8*s9*e, s3*s8*s9*e, s4*s8*s9*e, s5*s8*s9*e, s6*s8*s9*e, s7*s8*s9*e, s8^2*s9*e, s0*s9^2*e, s1*s9^2*e, s2*s9^2*e, s3*s9^2*e, s4*s9^2*e, s5*s9^2*e, s6*s9^2*e, s7*s9^2*e, s8*s9^2*e, s9^3*e, s0^2*s10*e, s0*s1*s10*e, s1^2*s10*e, s0*s2*s10*e, s1*s2*s10*e, s2^2*s10*e, s0*s3*s10*e, s1*s3*s10*e, s2*s3*s10*e, s3^2*s10*e, s0*s4*s10*e, s1*s4*s10*e, s2*s4*s10*e, s3*s4*s10*e, s4^2*s10*e, s0*s5*s10*e, s1*s5*s10*e, s2*s5*s10*e, s3*s5*s10*e, s4*s5*s10*e, s5^2*s10*e, s0*s6*s10*e, s1*s6*s10*e, s2*s6*s10*e, s3*s6*s10*e, s4*s6*s10*e, s5*s6*s10*e, s6^2*s10*e, s0*s7*s10*e, s1*s7*s10*e, s2*s7*s10*e, s3*s7*s10*e, s4*s7*s10*e, s5*s7*s10*e, s6*s7*s10*e, s7^2*s10*e, s0*s8*s10*e, s1*s8*s10*e, s2*s8*s10*e, s3*s8*s10*e, s4*s8*s10*e, s5*s8*s10*e, s6*s8*s10*e, s7*s8*s10*e, s8^2*s10*e, s0*s9*s10*e, s1*s9*s10*e, s2*s9*s10*e, s3*s9*s10*e, s4*s9*s10*e, s5*s9*s10*e, s6*s9*s10*e, s7*s9*s10*e, s8*s9*s10*e, s9^2*s10*e, s0*s10^2*e, s1*s10^2*e, s2*s10^2*e, s3*s10^2*e, s4*s10^2*e, s5*s10^2*e, s6*s10^2*e, s7*s10^2*e, s8*s10^2*e, s9*s10^2*e, s10^3*e, s0^2*s11*e, s0*s1*s11*e, s1^2*s11*e, s0*s2*s11*e, s1*s2*s11*e, s2^2*s11*e, s0*s3*s11*e, s1*s3*s11*e, s2*s3*s11*e, s3^2*s11*e, s0*s4*s11*e, s1*s4*s11*e, s2*s4*s11*e, s3*s4*s11*e, s4^2*s11*e, s0*s5*s11*e, s1*s5*s11*e, s2*s5*s11*e, s3*s5*s11*e, s4*s5*s11*e, s5^2*s11*e, s0*s6*s11*e, s1*s6*s11*e, s2*s6*s11*e, s3*s6*s11*e, s4*s6*s11*e, s5*s6*s11*e, s6^2*s11*e, s0*s7*s11*e, s1*s7*s11*e, s2*s7*s11*e, s3*s7*s11*e, s4*s7*s11*e, s5*s7*s11*e, s6*s7*s11*e, s7^2*s11*e, s0*s8*s11*e, s1*s8*s11*e, s2*s8*s11*e, s3*s8*s11*e, s4*s8*s11*e, s5*s8*s11*e, s6*s8*s11*e, s7*s8*s11*e, s8^2*s11*e, s0*s9*s11*e, s1*s9*s11*e, s2*s9*s11*e, s3*s9*s11*e, s4*s9*s11*e, s5*s9*s11*e, s6*s9*s11*e, s7*s9*s11*e, s8*s9*s11*e, s9^2*s11*e, s0*s10*s11*e, s1*s10*s11*e, s2*s10*s11*e, s3*s10*s11*e, s4*s10*s11*e, s5*s10*s11*e, s6*s10*s11*e, s7*s10*s11*e, s8*s10*s11*e, s9*s10*s11*e, s10^2*s11*e, s0*s11^2*e, s1*s11^2*e, s2*s11^2*e, s3*s11^2*e, s4*s11^2*e, s5*s11^2*e, s6*s11^2*e, s7*s11^2*e, s8*s11^2*e, s9*s11^2*e, s10*s11^2*e, s11^3*e, s0^2*s12*e, s0*s1*s12*e, s1^2*s12*e, s0*s2*s12*e, s1*s2*s12*e, s2^2*s12*e, s0*s3*s12*e, s1*s3*s12*e, s2*s3*s12*e, s3^2*s12*e, s0*s4*s12*e, s1*s4*s12*e, s2*s4*s12*e, s3*s4*s12*e, s4^2*s12*e, s0*s5*s12*e, s1*s5*s12*e, s2*s5*s12*e, s3*s5*s12*e, s4*s5*s12*e, s5^2*s12*e, s0*s6*s12*e, s1*s6*s12*e, s2*s6*s12*e, s3*s6*s12*e, s4*s6*s12*e, s5*s6*s12*e, s6^2*s12*e, s0*s7*s12*e, s1*s7*s12*e, s2*s7*s12*e, s3*s7*s12*e, s4*s7*s12*e, s5*s7*s12*e, s6*s7*s12*e, s7^2*s12*e, s0*s8*s12*e, s1*s8*s12*e, s2*s8*s12*e, s3*s8*s12*e, s4*s8*s12*e, s5*s8*s12*e, s6*s8*s12*e, s7*s8*s12*e, s8^2*s12*e, s0*s9*s12*e, s1*s9*s12*e, s2*s9*s12*e, s3*s9*s12*e, s4*s9*s12*e, s5*s9*s12*e, s6*s9*s12*e, s7*s9*s12*e, s8*s9*s12*e, s9^2*s12*e, s0*s10*s12*e, s1*s10*s12*e, s2*s10*s12*e, s3*s10*s12*e, s4*s10*s12*e, s5*s10*s12*e, s6*s10*s12*e, s7*s10*s12*e, s8*s10*s12*e, s9*s10*s12*e, s10^2*s12*e, s0*s11*s12*e, s1*s11*s12*e, s2*s11*s12*e, s3*s11*s12*e, s4*s11*s12*e, s5*s11*s12*e, s6*s11*s12*e, s7*s11*s12*e, s8*s11*s12*e, s9*s11*s12*e, s10*s11*s12*e, s11^2*s12*e, s0*s12^2*e, s1*s12^2*e, s2*s12^2*e, s3*s12^2*e, s4*s12^2*e, s5*s12^2*e, s6*s12^2*e, s7*s12^2*e, s8*s12^2*e, s9*s12^2*e, s10*s12^2*e, s11*s12^2*e, s12^3*e, s0^2*s13*e, s0*s1*s13*e, s1^2*s13*e, s0*s2*s13*e, s1*s2*s13*e, s2^2*s13*e, s0*s3*s13*e, s1*s3*s13*e, s2*s3*s13*e, s3^2*s13*e, s0*s4*s13*e, s1*s4*s13*e, s2*s4*s13*e, s3*s4*s13*e, s4^2*s13*e, s0*s5*s13*e, s1*s5*s13*e, s2*s5*s13*e, s3*s5*s13*e, s4*s5*s13*e, s5^2*s13*e, s0*s6*s13*e, s1*s6*s13*e, s2*s6*s13*e, s3*s6*s13*e, s4*s6*s13*e, s5*s6*s13*e, s6^2*s13*e, s0*s7*s13*e, s1*s7*s13*e, s2*s7*s13*e, s3*s7*s13*e, s4*s7*s13*e, s5*s7*s13*e, s6*s7*s13*e, s7^2*s13*e, s0*s8*s13*e, s1*s8*s13*e, s2*s8*s13*e, s3*s8*s13*e, s4*s8*s13*e, s5*s8*s13*e, s6*s8*s13*e, s7*s8*s13*e, s8^2*s13*e, s0*s9*s13*e, s1*s9*s13*e, s2*s9*s13*e, s3*s9*s13*e, s4*s9*s13*e, s5*s9*s13*e, s6*s9*s13*e, s7*s9*s13*e, s8*s9*s13*e, s9^2*s13*e, s0*s10*s13*e, s1*s10*s13*e, s2*s10*s13*e, s3*s10*s13*e, s4*s10*s13*e, s5*s10*s13*e, s6*s10*s13*e, s7*s10*s13*e, s8*s10*s13*e, s9*s10*s13*e, s10^2*s13*e, s0*s11*s13*e, s1*s11*s13*e, s2*s11*s13*e, s3*s11*s13*e, s4*s11*s13*e, s5*s11*s13*e, s6*s11*s13*e, s7*s11*s13*e, s8*s11*s13*e, s9*s11*s13*e, s10*s11*s13*e, s11^2*s13*e, s0*s12*s13*e, s1*s12*s13*e, s2*s12*s13*e, s3*s12*s13*e, s4*s12*s13*e, s5*s12*s13*e, s6*s12*s13*e, s7*s12*s13*e, s8*s12*s13*e, s9*s12*s13*e, s10*s12*s13*e, s11*s12*s13*e, s12^2*s13*e, s0*s13^2*e, s1*s13^2*e, s2*s13^2*e, s3*s13^2*e, s4*s13^2*e, s5*s13^2*e, s6*s13^2*e, s7*s13^2*e, s8*s13^2*e, s9*s13^2*e, s10*s13^2*e, s11*s13^2*e, s12*s13^2*e, s13^3*e, s0^2*e^2, s0*s1*e^2, s1^2*e^2, s0*s2*e^2, s1*s2*e^2, s2^2*e^2, s0*s3*e^2, s1*s3*e^2, s2*s3*e^2, s3^2*e^2, s0*s4*e^2, s1*s4*e^2, s2*s4*e^2, s3*s4*e^2, s4^2*e^2, s0*s5*e^2, s1*s5*e^2, s2*s5*e^2, s3*s5*e^2, s4*s5*e^2, s5^2*e^2, s0*s6*e^2, s1*s6*e^2, s2*s6*e^2, s3*s6*e^2, s4*s6*e^2, s5*s6*e^2, s6^2*e^2, s0*s7*e^2, s1*s7*e^2, s2*s7*e^2, s3*s7*e^2, s4*s7*e^2, s5*s7*e^2, s6*s7*e^2, s7^2*e^2, s0*s8*e^2, s1*s8*e^2, s2*s8*e^2, s3*s8*e^2, s4*s8*e^2, s5*s8*e^2, s6*s8*e^2, s7*s8*e^2, s8^2*e^2, s0*s9*e^2, s1*s9*e^2, s2*s9*e^2, s3*s9*e^2, s4*s9*e^2, s5*s9*e^2, s6*s9*e^2, s7*s9*e^2, s8*s9*e^2, s9^2*e^2, s0*s10*e^2, s1*s10*e^2, s2*s10*e^2, s3*s10*e^2, s4*s10*e^2, s5*s10*e^2, s6*s10*e^2, s7*s10*e^2, s8*s10*e^2, s9*s10*e^2, s10^2*e^2, s0*s11*e^2, s1*s11*e^2, s2*s11*e^2, s3*s11*e^2, s4*s11*e^2, s5*s11*e^2, s6*s11*e^2, s7*s11*e^2, s8*s11*e^2, s9*s11*e^2, s10*s11*e^2, s11^2*e^2, s0*s12*e^2, s1*s12*e^2, s2*s12*e^2, s3*s12*e^2, s4*s12*e^2, s5*s12*e^2, s6*s12*e^2, s7*s12*e^2, s8*s12*e^2, s9*s12*e^2, s10*s12*e^2, s11*s12*e^2, s12^2*e^2, s0*s13*e^2, s1*s13*e^2, s2*s13*e^2, s3*s13*e^2, s4*s13*e^2, s5*s13*e^2, s6*s13*e^2, s7*s13*e^2, s8*s13*e^2, s9*s13*e^2, s10*s13*e^2, s11*s13*e^2, s12*s13*e^2, s13^2*e^2, s0*e^3, s1*e^3, s2*e^3, s3*e^3, s4*e^3, s5*e^3, s6*e^3, s7*e^3, s8*e^3, s9*e^3, s10*e^3, s11*e^3, s12*e^3, s13*e^3, e^4, s0^3*b, s0^2*s1*b, s0*s1^2*b, s1^3*b, s0^2*s2*b, s0*s1*s2*b, s1^2*s2*b, s0*s2^2*b, s1*s2^2*b, s2^3*b, s0^2*s3*b, s0*s1*s3*b, s1^2*s3*b, s0*s2*s3*b, s1*s2*s3*b, s2^2*s3*b, s0*s3^2*b, s1*s3^2*b, s2*s3^2*b, s3^3*b, s0^2*s4*b, s0*s1*s4*b, s1^2*s4*b, s0*s2*s4*b, s1*s2*s4*b, s2^2*s4*b, s0*s3*s4*b, s1*s3*s4*b, s2*s3*s4*b, s3^2*s4*b, s0*s4^2*b, s1*s4^2*b, s2*s4^2*b, s3*s4^2*b, s4^3*b, s0^2*s5*b, s0*s1*s5*b, s1^2*s5*b, s0*s2*s5*b, s1*s2*s5*b, s2^2*s5*b, s0*s3*s5*b, s1*s3*s5*b, s2*s3*s5*b, s3^2*s5*b, s0*s4*s5*b, s1*s4*s5*b, s2*s4*s5*b, s3*s4*s5*b, s4^2*s5*b, s0*s5^2*b, s1*s5^2*b, s2*s5^2*b, s3*s5^2*b, s4*s5^2*b, s5^3*b, s0^2*s6*b, s0*s1*s6*b, s1^2*s6*b, s0*s2*s6*b, s1*s2*s6*b, s2^2*s6*b, s0*s3*s6*b, s1*s3*s6*b, s2*s3*s6*b, s3^2*s6*b, s0*s4*s6*b, s1*s4*s6*b, s2*s4*s6*b, s3*s4*s6*b, s4^2*s6*b, s0*s5*s6*b, s1*s5*s6*b, s2*s5*s6*b, s3*s5*s6*b, s4*s5*s6*b, s5^2*s6*b, s0*s6^2*b, s1*s6^2*b, s2*s6^2*b, s3*s6^2*b, s4*s6^2*b, s5*s6^2*b, s6^3*b, s0^2*s7*b, s0*s1*s7*b, s1^2*s7*b, s0*s2*s7*b, s1*s2*s7*b, s2^2*s7*b, s0*s3*s7*b, s1*s3*s7*b, s2*s3*s7*b, s3^2*s7*b, s0*s4*s7*b, s1*s4*s7*b, s2*s4*s7*b, s3*s4*s7*b, s4^2*s7*b, s0*s5*s7*b, s1*s5*s7*b, s2*s5*s7*b, s3*s5*s7*b, s4*s5*s7*b, s5^2*s7*b, s0*s6*s7*b, s1*s6*s7*b, s2*s6*s7*b, s3*s6*s7*b, s4*s6*s7*b, s5*s6*s7*b, s6^2*s7*b, s0*s7^2*b, s1*s7^2*b, s2*s7^2*b, s3*s7^2*b, s4*s7^2*b, s5*s7^2*b, s6*s7^2*b, s7^3*b, s0^2*s8*b, s0*s1*s8*b, s1^2*s8*b, s0*s2*s8*b, s1*s2*s8*b, s2^2*s8*b, s0*s3*s8*b, s1*s3*s8*b, s2*s3*s8*b, s3^2*s8*b, s0*s4*s8*b, s1*s4*s8*b, s2*s4*s8*b, s3*s4*s8*b, s4^2*s8*b, s0*s5*s8*b, s1*s5*s8*b, s2*s5*s8*b, s3*s5*s8*b, s4*s5*s8*b, s5^2*s8*b, s0*s6*s8*b, s1*s6*s8*b, s2*s6*s8*b, s3*s6*s8*b, s4*s6*s8*b, s5*s6*s8*b, s6^2*s8*b, s0*s7*s8*b, s1*s7*s8*b, s2*s7*s8*b, s3*s7*s8*b, s4*s7*s8*b, s5*s7*s8*b, s6*s7*s8*b, s7^2*s8*b, s0*s8^2*b, s1*s8^2*b, s2*s8^2*b, s3*s8^2*b, s4*s8^2*b, s5*s8^2*b, s6*s8^2*b, s7*s8^2*b, s8^3*b, s0^2*s9*b, s0*s1*s9*b, s1^2*s9*b, s0*s2*s9*b, s1*s2*s9*b, s2^2*s9*b, s0*s3*s9*b, s1*s3*s9*b, s2*s3*s9*b, s3^2*s9*b, s0*s4*s9*b, s1*s4*s9*b, s2*s4*s9*b, s3*s4*s9*b, s4^2*s9*b, s0*s5*s9*b, s1*s5*s9*b, s2*s5*s9*b, s3*s5*s9*b, s4*s5*s9*b, s5^2*s9*b, s0*s6*s9*b, s1*s6*s9*b, s2*s6*s9*b, s3*s6*s9*b, s4*s6*s9*b, s5*s6*s9*b, s6^2*s9*b, s0*s7*s9*b, s1*s7*s9*b, s2*s7*s9*b, s3*s7*s9*b, s4*s7*s9*b, s5*s7*s9*b, s6*s7*s9*b, s7^2*s9*b, s0*s8*s9*b, s1*s8*s9*b, s2*s8*s9*b, s3*s8*s9*b, s4*s8*s9*b, s5*s8*s9*b, s6*s8*s9*b, s7*s8*s9*b, s8^2*s9*b, s0*s9^2*b, s1*s9^2*b, s2*s9^2*b, s3*s9^2*b, s4*s9^2*b, s5*s9^2*b, s6*s9^2*b, s7*s9^2*b, s8*s9^2*b, s9^3*b, s0^2*s10*b, s0*s1*s10*b, s1^2*s10*b, s0*s2*s10*b, s1*s2*s10*b, s2^2*s10*b, s0*s3*s10*b, s1*s3*s10*b, s2*s3*s10*b, s3^2*s10*b, s0*s4*s10*b, s1*s4*s10*b, s2*s4*s10*b, s3*s4*s10*b, s4^2*s10*b, s0*s5*s10*b, s1*s5*s10*b, s2*s5*s10*b, s3*s5*s10*b, s4*s5*s10*b, s5^2*s10*b, s0*s6*s10*b, s1*s6*s10*b, s2*s6*s10*b, s3*s6*s10*b, s4*s6*s10*b, s5*s6*s10*b, s6^2*s10*b, s0*s7*s10*b, s1*s7*s10*b, s2*s7*s10*b, s3*s7*s10*b, s4*s7*s10*b, s5*s7*s10*b, s6*s7*s10*b, s7^2*s10*b, s0*s8*s10*b, s1*s8*s10*b, s2*s8*s10*b, s3*s8*s10*b, s4*s8*s10*b, s5*s8*s10*b, s6*s8*s10*b, s7*s8*s10*b, s8^2*s10*b, s0*s9*s10*b, s1*s9*s10*b, s2*s9*s10*b, s3*s9*s10*b, s4*s9*s10*b, s5*s9*s10*b, s6*s9*s10*b, s7*s9*s10*b, s8*s9*s10*b, s9^2*s10*b, s0*s10^2*b, s1*s10^2*b, s2*s10^2*b, s3*s10^2*b, s4*s10^2*b, s5*s10^2*b, s6*s10^2*b, s7*s10^2*b, s8*s10^2*b, s9*s10^2*b, s10^3*b, s0^2*s11*b, s0*s1*s11*b, s1^2*s11*b, s0*s2*s11*b, s1*s2*s11*b, s2^2*s11*b, s0*s3*s11*b, s1*s3*s11*b, s2*s3*s11*b, s3^2*s11*b, s0*s4*s11*b, s1*s4*s11*b, s2*s4*s11*b, s3*s4*s11*b, s4^2*s11*b, s0*s5*s11*b, s1*s5*s11*b, s2*s5*s11*b, s3*s5*s11*b, s4*s5*s11*b, s5^2*s11*b, s0*s6*s11*b, s1*s6*s11*b, s2*s6*s11*b, s3*s6*s11*b, s4*s6*s11*b, s5*s6*s11*b, s6^2*s11*b, s0*s7*s11*b, s1*s7*s11*b, s2*s7*s11*b, s3*s7*s11*b, s4*s7*s11*b, s5*s7*s11*b, s6*s7*s11*b, s7^2*s11*b, s0*s8*s11*b, s1*s8*s11*b, s2*s8*s11*b, s3*s8*s11*b, s4*s8*s11*b, s5*s8*s11*b, s6*s8*s11*b, s7*s8*s11*b, s8^2*s11*b, s0*s9*s11*b, s1*s9*s11*b, s2*s9*s11*b, s3*s9*s11*b, s4*s9*s11*b, s5*s9*s11*b, s6*s9*s11*b, s7*s9*s11*b, s8*s9*s11*b, s9^2*s11*b, s0*s10*s11*b, s1*s10*s11*b, s2*s10*s11*b, s3*s10*s11*b, s4*s10*s11*b, s5*s10*s11*b, s6*s10*s11*b, s7*s10*s11*b, s8*s10*s11*b, s9*s10*s11*b, s10^2*s11*b, s0*s11^2*b, s1*s11^2*b, s2*s11^2*b, s3*s11^2*b, s4*s11^2*b, s5*s11^2*b, s6*s11^2*b, s7*s11^2*b, s8*s11^2*b, s9*s11^2*b, s10*s11^2*b, s11^3*b, s0^2*s12*b, s0*s1*s12*b, s1^2*s12*b, s0*s2*s12*b, s1*s2*s12*b, s2^2*s12*b, s0*s3*s12*b, s1*s3*s12*b, s2*s3*s12*b, s3^2*s12*b, s0*s4*s12*b, s1*s4*s12*b, s2*s4*s12*b, s3*s4*s12*b, s4^2*s12*b, s0*s5*s12*b, s1*s5*s12*b, s2*s5*s12*b, s3*s5*s12*b, s4*s5*s12*b, s5^2*s12*b, s0*s6*s12*b, s1*s6*s12*b, s2*s6*s12*b, s3*s6*s12*b, s4*s6*s12*b, s5*s6*s12*b, s6^2*s12*b, s0*s7*s12*b, s1*s7*s12*b, s2*s7*s12*b, s3*s7*s12*b, s4*s7*s12*b, s5*s7*s12*b, s6*s7*s12*b, s7^2*s12*b, s0*s8*s12*b, s1*s8*s12*b, s2*s8*s12*b, s3*s8*s12*b, s4*s8*s12*b, s5*s8*s12*b, s6*s8*s12*b, s7*s8*s12*b, s8^2*s12*b, s0*s9*s12*b, s1*s9*s12*b, s2*s9*s12*b, s3*s9*s12*b, s4*s9*s12*b, s5*s9*s12*b, s6*s9*s12*b, s7*s9*s12*b, s8*s9*s12*b, s9^2*s12*b, s0*s10*s12*b, s1*s10*s12*b, s2*s10*s12*b, s3*s10*s12*b, s4*s10*s12*b, s5*s10*s12*b, s6*s10*s12*b, s7*s10*s12*b, s8*s10*s12*b, s9*s10*s12*b, s10^2*s12*b, s0*s11*s12*b, s1*s11*s12*b, s2*s11*s12*b, s3*s11*s12*b, s4*s11*s12*b, s5*s11*s12*b, s6*s11*s12*b, s7*s11*s12*b, s8*s11*s12*b, s9*s11*s12*b, s10*s11*s12*b, s11^2*s12*b, s0*s12^2*b, s1*s12^2*b, s2*s12^2*b, s3*s12^2*b, s4*s12^2*b, s5*s12^2*b, s6*s12^2*b, s7*s12^2*b, s8*s12^2*b, s9*s12^2*b, s10*s12^2*b, s11*s12^2*b, s12^3*b, s0^2*s13*b, s0*s1*s13*b, s1^2*s13*b, s0*s2*s13*b, s1*s2*s13*b, s2^2*s13*b, s0*s3*s13*b, s1*s3*s13*b, s2*s3*s13*b, s3^2*s13*b, s0*s4*s13*b, s1*s4*s13*b, s2*s4*s13*b, s3*s4*s13*b, s4^2*s13*b, s0*s5*s13*b, s1*s5*s13*b, s2*s5*s13*b, s3*s5*s13*b, s4*s5*s13*b, s5^2*s13*b, s0*s6*s13*b, s1*s6*s13*b, s2*s6*s13*b, s3*s6*s13*b, s4*s6*s13*b, s5*s6*s13*b, s6^2*s13*b, s0*s7*s13*b, s1*s7*s13*b, s2*s7*s13*b, s3*s7*s13*b, s4*s7*s13*b, s5*s7*s13*b, s6*s7*s13*b, s7^2*s13*b, s0*s8*s13*b, s1*s8*s13*b, s2*s8*s13*b, s3*s8*s13*b, s4*s8*s13*b, s5*s8*s13*b, s6*s8*s13*b, s7*s8*s13*b, s8^2*s13*b, s0*s9*s13*b, s1*s9*s13*b, s2*s9*s13*b, s3*s9*s13*b, s4*s9*s13*b, s5*s9*s13*b, s6*s9*s13*b, s7*s9*s13*b, s8*s9*s13*b, s9^2*s13*b, s0*s10*s13*b, s1*s10*s13*b, s2*s10*s13*b, s3*s10*s13*b, s4*s10*s13*b, s5*s10*s13*b, s6*s10*s13*b, s7*s10*s13*b, s8*s10*s13*b, s9*s10*s13*b, s10^2*s13*b, s0*s11*s13*b, s1*s11*s13*b, s2*s11*s13*b, s3*s11*s13*b, s4*s11*s13*b, s5*s11*s13*b, s6*s11*s13*b, s7*s11*s13*b, s8*s11*s13*b, s9*s11*s13*b, s10*s11*s13*b, s11^2*s13*b, s0*s12*s13*b, s1*s12*s13*b, s2*s12*s13*b, s3*s12*s13*b, s4*s12*s13*b, s5*s12*s13*b, s6*s12*s13*b, s7*s12*s13*b, s8*s12*s13*b, s9*s12*s13*b, s10*s12*s13*b, s11*s12*s13*b, s12^2*s13*b, s0*s13^2*b, s1*s13^2*b, s2*s13^2*b, s3*s13^2*b, s4*s13^2*b, s5*s13^2*b, s6*s13^2*b, s7*s13^2*b, s8*s13^2*b, s9*s13^2*b, s10*s13^2*b, s11*s13^2*b, s12*s13^2*b, s13^3*b, s0^2*e*b, s0*s1*e*b, s1^2*e*b, s0*s2*e*b, s1*s2*e*b, s2^2*e*b, s0*s3*e*b, s1*s3*e*b, s2*s3*e*b, s3^2*e*b, s0*s4*e*b, s1*s4*e*b, s2*s4*e*b, s3*s4*e*b, s4^2*e*b, s0*s5*e*b, s1*s5*e*b, s2*s5*e*b, s3*s5*e*b, s4*s5*e*b, s5^2*e*b, s0*s6*e*b, s1*s6*e*b, s2*s6*e*b, s3*s6*e*b, s4*s6*e*b, s5*s6*e*b, s6^2*e*b, s0*s7*e*b, s1*s7*e*b, s2*s7*e*b, s3*s7*e*b, s4*s7*e*b, s5*s7*e*b, s6*s7*e*b, s7^2*e*b, s0*s8*e*b, s1*s8*e*b, s2*s8*e*b, s3*s8*e*b, s4*s8*e*b, s5*s8*e*b, s6*s8*e*b, s7*s8*e*b, s8^2*e*b, s0*s9*e*b, s1*s9*e*b, s2*s9*e*b, s3*s9*e*b, s4*s9*e*b, s5*s9*e*b, s6*s9*e*b, s7*s9*e*b, s8*s9*e*b, s9^2*e*b, s0*s10*e*b, s1*s10*e*b, s2*s10*e*b, s3*s10*e*b, s4*s10*e*b, s5*s10*e*b, s6*s10*e*b, s7*s10*e*b, s8*s10*e*b, s9*s10*e*b, s10^2*e*b, s0*s11*e*b, s1*s11*e*b, s2*s11*e*b, s3*s11*e*b, s4*s11*e*b, s5*s11*e*b, s6*s11*e*b, s7*s11*e*b, s8*s11*e*b, s9*s11*e*b, s10*s11*e*b, s11^2*e*b, s0*s12*e*b, s1*s12*e*b, s2*s12*e*b, s3*s12*e*b, s4*s12*e*b, s5*s12*e*b, s6*s12*e*b, s7*s12*e*b, s8*s12*e*b, s9*s12*e*b, s10*s12*e*b, s11*s12*e*b, s12^2*e*b, s0*s13*e*b, s1*s13*e*b, s2*s13*e*b, s3*s13*e*b, s4*s13*e*b, s5*s13*e*b, s6*s13*e*b, s7*s13*e*b, s8*s13*e*b, s9*s13*e*b, s10*s13*e*b, s11*s13*e*b, s12*s13*e*b, s13^2*e*b, s0*e^2*b, s1*e^2*b, s2*e^2*b, s3*e^2*b, s4*e^2*b, s5*e^2*b, s6*e^2*b, s7*e^2*b, s8*e^2*b, s9*e^2*b, s10*e^2*b, s11*e^2*b, s12*e^2*b, s13*e^2*b, e^3*b, s0^2*b^2, s0*s1*b^2, s1^2*b^2, s0*s2*b^2, s1*s2*b^2, s2^2*b^2, s0*s3*b^2, s1*s3*b^2, s2*s3*b^2, s3^2*b^2, s0*s4*b^2, s1*s4*b^2, s2*s4*b^2, s3*s4*b^2, s4^2*b^2, s0*s5*b^2, s1*s5*b^2, s2*s5*b^2, s3*s5*b^2, s4*s5*b^2, s5^2*b^2, s0*s6*b^2, s1*s6*b^2, s2*s6*b^2, s3*s6*b^2, s4*s6*b^2, s5*s6*b^2, s6^2*b^2, s0*s7*b^2, s1*s7*b^2, s2*s7*b^2, s3*s7*b^2, s4*s7*b^2, s5*s7*b^2, s6*s7*b^2, s7^2*b^2, s0*s8*b^2, s1*s8*b^2, s2*s8*b^2, s3*s8*b^2, s4*s8*b^2, s5*s8*b^2, s6*s8*b^2, s7*s8*b^2, s8^2*b^2, s0*s9*b^2, s1*s9*b^2, s2*s9*b^2, s3*s9*b^2, s4*s9*b^2, s5*s9*b^2, s6*s9*b^2, s7*s9*b^2, s8*s9*b^2, s9^2*b^2, s0*s10*b^2, s1*s10*b^2, s2*s10*b^2, s3*s10*b^2, s4*s10*b^2, s5*s10*b^2, s6*s10*b^2, s7*s10*b^2, s8*s10*b^2, s9*s10*b^2, s10^2*b^2, s0*s11*b^2, s1*s11*b^2, s2*s11*b^2, s3*s11*b^2, s4*s11*b^2, s5*s11*b^2, s6*s11*b^2, s7*s11*b^2, s8*s11*b^2, s9*s11*b^2, s10*s11*b^2, s11^2*b^2, s0*s12*b^2, s1*s12*b^2, s2*s12*b^2, s3*s12*b^2, s4*s12*b^2, s5*s12*b^2, s6*s12*b^2, s7*s12*b^2, s8*s12*b^2, s9*s12*b^2, s10*s12*b^2, s11*s12*b^2, s12^2*b^2, s0*s13*b^2, s1*s13*b^2, s2*s13*b^2, s3*s13*b^2, s4*s13*b^2, s5*s13*b^2, s6*s13*b^2, s7*s13*b^2, s8*s13*b^2, s9*s13*b^2, s10*s13*b^2, s11*s13*b^2, s12*s13*b^2, s13^2*b^2, s0*e*b^2, s1*e*b^2, s2*e*b^2, s3*e*b^2, s4*e*b^2, s5*e*b^2, s6*e*b^2, s7*e*b^2, s8*e*b^2, s9*e*b^2, s10*e*b^2, s11*e*b^2, s12*e*b^2, s13*e*b^2, e^2*b^2, s0*b^3, s1*b^3, s2*b^3, s3*b^3, s4*b^3, s5*b^3, s6*b^3, s7*b^3, s8*b^3, s9*b^3, s10*b^3, s11*b^3, s12*b^3, s13*b^3, e*b^3, b^4, s0^3, s0^2*s1, s0*s1^2, s1^3, s0^2*s2, s0*s1*s2, s1^2*s2, s0*s2^2, s1*s2^2, s2^3, s0^2*s3, s0*s1*s3, s1^2*s3, s0*s2*s3, s1*s2*s3, s2^2*s3, s0*s3^2, s1*s3^2, s2*s3^2, s3^3, s0^2*s4, s0*s1*s4, s1^2*s4, s0*s2*s4, s1*s2*s4, s2^2*s4, s0*s3*s4, s1*s3*s4, s2*s3*s4, s3^2*s4, s0*s4^2, s1*s4^2, s2*s4^2, s3*s4^2, s4^3, s0^2*s5, s0*s1*s5, s1^2*s5, s0*s2*s5, s1*s2*s5, s2^2*s5, s0*s3*s5, s1*s3*s5, s2*s3*s5, s3^2*s5, s0*s4*s5, s1*s4*s5, s2*s4*s5, s3*s4*s5, s4^2*s5, s0*s5^2, s1*s5^2, s2*s5^2, s3*s5^2, s4*s5^2, s5^3, s0^2*s6, s0*s1*s6, s1^2*s6, s0*s2*s6, s1*s2*s6, s2^2*s6, s0*s3*s6, s1*s3*s6, s2*s3*s6, s3^2*s6, s0*s4*s6, s1*s4*s6, s2*s4*s6, s3*s4*s6, s4^2*s6, s0*s5*s6, s1*s5*s6, s2*s5*s6, s3*s5*s6, s4*s5*s6, s5^2*s6, s0*s6^2, s1*s6^2, s2*s6^2, s3*s6^2, s4*s6^2, s5*s6^2, s6^3, s0^2*s7, s0*s1*s7, s1^2*s7, s0*s2*s7, s1*s2*s7, s2^2*s7, s0*s3*s7, s1*s3*s7, s2*s3*s7, s3^2*s7, s0*s4*s7, s1*s4*s7, s2*s4*s7, s3*s4*s7, s4^2*s7, s0*s5*s7, s1*s5*s7, s2*s5*s7, s3*s5*s7, s4*s5*s7, s5^2*s7, s0*s6*s7, s1*s6*s7, s2*s6*s7, s3*s6*s7, s4*s6*s7, s5*s6*s7, s6^2*s7, s0*s7^2, s1*s7^2, s2*s7^2, s3*s7^2, s4*s7^2, s5*s7^2, s6*s7^2, s7^3, s0^2*s8, s0*s1*s8, s1^2*s8, s0*s2*s8, s1*s2*s8, s2^2*s8, s0*s3*s8, s1*s3*s8, s2*s3*s8, s3^2*s8, s0*s4*s8, s1*s4*s8, s2*s4*s8, s3*s4*s8, s4^2*s8, s0*s5*s8, s1*s5*s8, s2*s5*s8, s3*s5*s8, s4*s5*s8, s5^2*s8, s0*s6*s8, s1*s6*s8, s2*s6*s8, s3*s6*s8, s4*s6*s8, s5*s6*s8, s6^2*s8, s0*s7*s8, s1*s7*s8, s2*s7*s8, s3*s7*s8, s4*s7*s8, s5*s7*s8, s6*s7*s8, s7^2*s8, s0*s8^2, s1*s8^2, s2*s8^2, s3*s8^2, s4*s8^2, s5*s8^2, s6*s8^2, s7*s8^2, s8^3, s0^2*s9, s0*s1*s9, s1^2*s9, s0*s2*s9, s1*s2*s9, s2^2*s9, s0*s3*s9, s1*s3*s9, s2*s3*s9, s3^2*s9, s0*s4*s9, s1*s4*s9, s2*s4*s9, s3*s4*s9, s4^2*s9, s0*s5*s9, s1*s5*s9, s2*s5*s9, s3*s5*s9, s4*s5*s9, s5^2*s9, s0*s6*s9, s1*s6*s9, s2*s6*s9, s3*s6*s9, s4*s6*s9, s5*s6*s9, s6^2*s9, s0*s7*s9, s1*s7*s9, s2*s7*s9, s3*s7*s9, s4*s7*s9, s5*s7*s9, s6*s7*s9, s7^2*s9, s0*s8*s9, s1*s8*s9, s2*s8*s9, s3*s8*s9, s4*s8*s9, s5*s8*s9, s6*s8*s9, s7*s8*s9, s8^2*s9, s0*s9^2, s1*s9^2, s2*s9^2, s3*s9^2, s4*s9^2, s5*s9^2, s6*s9^2, s7*s9^2, s8*s9^2, s9^3, s0^2*s10, s0*s1*s10, s1^2*s10, s0*s2*s10, s1*s2*s10, s2^2*s10, s0*s3*s10, s1*s3*s10, s2*s3*s10, s3^2*s10, s0*s4*s10, s1*s4*s10, s2*s4*s10, s3*s4*s10, s4^2*s10, s0*s5*s10, s1*s5*s10, s2*s5*s10, s3*s5*s10, s4*s5*s10, s5^2*s10, s0*s6*s10, s1*s6*s10, s2*s6*s10, s3*s6*s10, s4*s6*s10, s5*s6*s10, s6^2*s10, s0*s7*s10, s1*s7*s10, s2*s7*s10, s3*s7*s10, s4*s7*s10, s5*s7*s10, s6*s7*s10, s7^2*s10, s0*s8*s10, s1*s8*s10, s2*s8*s10, s3*s8*s10, s4*s8*s10, s5*s8*s10, s6*s8*s10, s7*s8*s10, s8^2*s10, s0*s9*s10, s1*s9*s10, s2*s9*s10, s3*s9*s10, s4*s9*s10, s5*s9*s10, s6*s9*s10, s7*s9*s10, s8*s9*s10, s9^2*s10, s0*s10^2, s1*s10^2, s2*s10^2, s3*s10^2, s4*s10^2, s5*s10^2, s6*s10^2, s7*s10^2, s8*s10^2, s9*s10^2, s10^3, s0^2*s11, s0*s1*s11, s1^2*s11, s0*s2*s11, s1*s2*s11, s2^2*s11, s0*s3*s11, s1*s3*s11, s2*s3*s11, s3^2*s11, s0*s4*s11, s1*s4*s11, s2*s4*s11, s3*s4*s11, s4^2*s11, s0*s5*s11, s1*s5*s11, s2*s5*s11, s3*s5*s11, s4*s5*s11, s5^2*s11, s0*s6*s11, s1*s6*s11, s2*s6*s11, s3*s6*s11, s4*s6*s11, s5*s6*s11, s6^2*s11, s0*s7*s11, s1*s7*s11, s2*s7*s11, s3*s7*s11, s4*s7*s11, s5*s7*s11, s6*s7*s11, s7^2*s11, s0*s8*s11, s1*s8*s11, s2*s8*s11, s3*s8*s11, s4*s8*s11, s5*s8*s11, s6*s8*s11, s7*s8*s11, s8^2*s11, s0*s9*s11, s1*s9*s11, s2*s9*s11, s3*s9*s11, s4*s9*s11, s5*s9*s11, s6*s9*s11, s7*s9*s11, s8*s9*s11, s9^2*s11, s0*s10*s11, s1*s10*s11, s2*s10*s11, s3*s10*s11, s4*s10*s11, s5*s10*s11, s6*s10*s11, s7*s10*s11, s8*s10*s11, s9*s10*s11, s10^2*s11, s0*s11^2, s1*s11^2, s2*s11^2, s3*s11^2, s4*s11^2, s5*s11^2, s6*s11^2, s7*s11^2, s8*s11^2, s9*s11^2, s10*s11^2, s11^3, s0^2*s12, s0*s1*s12, s1^2*s12, s0*s2*s12, s1*s2*s12, s2^2*s12, s0*s3*s12, s1*s3*s12, s2*s3*s12, s3^2*s12, s0*s4*s12, s1*s4*s12, s2*s4*s12, s3*s4*s12, s4^2*s12, s0*s5*s12, s1*s5*s12, s2*s5*s12, s3*s5*s12, s4*s5*s12, s5^2*s12, s0*s6*s12, s1*s6*s12, s2*s6*s12, s3*s6*s12, s4*s6*s12, s5*s6*s12, s6^2*s12, s0*s7*s12, s1*s7*s12, s2*s7*s12, s3*s7*s12, s4*s7*s12, s5*s7*s12, s6*s7*s12, s7^2*s12, s0*s8*s12, s1*s8*s12, s2*s8*s12, s3*s8*s12, s4*s8*s12, s5*s8*s12, s6*s8*s12, s7*s8*s12, s8^2*s12, s0*s9*s12, s1*s9*s12, s2*s9*s12, s3*s9*s12, s4*s9*s12, s5*s9*s12, s6*s9*s12, s7*s9*s12, s8*s9*s12, s9^2*s12, s0*s10*s12, s1*s10*s12, s2*s10*s12, s3*s10*s12, s4*s10*s12, s5*s10*s12, s6*s10*s12, s7*s10*s12, s8*s10*s12, s9*s10*s12, s10^2*s12, s0*s11*s12, s1*s11*s12, s2*s11*s12, s3*s11*s12, s4*s11*s12, s5*s11*s12, s6*s11*s12, s7*s11*s12, s8*s11*s12, s9*s11*s12, s10*s11*s12, s11^2*s12, s0*s12^2, s1*s12^2, s2*s12^2, s3*s12^2, s4*s12^2, s5*s12^2, s6*s12^2, s7*s12^2, s8*s12^2, s9*s12^2, s10*s12^2, s11*s12^2, s12^3, s0^2*s13, s0*s1*s13, s1^2*s13, s0*s2*s13, s1*s2*s13, s2^2*s13, s0*s3*s13, s1*s3*s13, s2*s3*s13, s3^2*s13, s0*s4*s13, s1*s4*s13, s2*s4*s13, s3*s4*s13, s4^2*s13, s0*s5*s13, s1*s5*s13, s2*s5*s13, s3*s5*s13, s4*s5*s13, s5^2*s13, s0*s6*s13, s1*s6*s13, s2*s6*s13, s3*s6*s13, s4*s6*s13, s5*s6*s13, s6^2*s13, s0*s7*s13, s1*s7*s13, s2*s7*s13, s3*s7*s13, s4*s7*s13, s5*s7*s13, s6*s7*s13, s7^2*s13, s0*s8*s13, s1*s8*s13, s2*s8*s13, s3*s8*s13, s4*s8*s13, s5*s8*s13, s6*s8*s13, s7*s8*s13, s8^2*s13, s0*s9*s13, s1*s9*s13, s2*s9*s13, s3*s9*s13, s4*s9*s13, s5*s9*s13, s6*s9*s13, s7*s9*s13, s8*s9*s13, s9^2*s13, s0*s10*s13, s1*s10*s13, s2*s10*s13, s3*s10*s13, s4*s10*s13, s5*s10*s13, s6*s10*s13, s7*s10*s13, s8*s10*s13, s9*s10*s13, s10^2*s13, s0*s11*s13, s1*s11*s13, s2*s11*s13, s3*s11*s13, s4*s11*s13, s5*s11*s13, s6*s11*s13, s7*s11*s13, s8*s11*s13, s9*s11*s13, s10*s11*s13, s11^2*s13, s0*s12*s13, s1*s12*s13, s2*s12*s13, s3*s12*s13, s4*s12*s13, s5*s12*s13, s6*s12*s13, s7*s12*s13, s8*s12*s13, s9*s12*s13, s10*s12*s13, s11*s12*s13, s12^2*s13, s0*s13^2, s1*s13^2, s2*s13^2, s3*s13^2, s4*s13^2, s5*s13^2, s6*s13^2, s7*s13^2, s8*s13^2, s9*s13^2, s10*s13^2, s11*s13^2, s12*s13^2, s13^3, s0^2*e, s0*s1*e, s1^2*e, s0*s2*e, s1*s2*e, s2^2*e, s0*s3*e, s1*s3*e, s2*s3*e, s3^2*e, s0*s4*e, s1*s4*e, s2*s4*e, s3*s4*e, s4^2*e, s0*s5*e, s1*s5*e, s2*s5*e, s3*s5*e, s4*s5*e, s5^2*e, s0*s6*e, s1*s6*e, s2*s6*e, s3*s6*e, s4*s6*e, s5*s6*e, s6^2*e, s0*s7*e, s1*s7*e, s2*s7*e, s3*s7*e, s4*s7*e, s5*s7*e, s6*s7*e, s7^2*e, s0*s8*e, s1*s8*e, s2*s8*e, s3*s8*e, s4*s8*e, s5*s8*e, s6*s8*e, s7*s8*e, s8^2*e, s0*s9*e, s1*s9*e, s2*s9*e, s3*s9*e, s4*s9*e, s5*s9*e, s6*s9*e, s7*s9*e, s8*s9*e, s9^2*e, s0*s10*e, s1*s10*e, s2*s10*e, s3*s10*e, s4*s10*e, s5*s10*e, s6*s10*e, s7*s10*e, s8*s10*e, s9*s10*e, s10^2*e, s0*s11*e, s1*s11*e, s2*s11*e, s3*s11*e, s4*s11*e, s5*s11*e, s6*s11*e, s7*s11*e, s8*s11*e, s9*s11*e, s10*s11*e, s11^2*e, s0*s12*e, s1*s12*e, s2*s12*e, s3*s12*e, s4*s12*e, s5*s12*e, s6*s12*e, s7*s12*e, s8*s12*e, s9*s12*e, s10*s12*e, s11*s12*e, s12^2*e, s0*s13*e, s1*s13*e, s2*s13*e, s3*s13*e, s4*s13*e, s5*s13*e, s6*s13*e, s7*s13*e, s8*s13*e, s9*s13*e, s10*s13*e, s11*s13*e, s12*s13*e, s13^2*e, s0*e^2, s1*e^2, s2*e^2, s3*e^2, s4*e^2, s5*e^2, s6*e^2, s7*e^2, s8*e^2, s9*e^2, s10*e^2, s11*e^2, s12*e^2, s13*e^2, e^3, s0^2*b, s0*s1*b, s1^2*b, s0*s2*b, s1*s2*b, s2^2*b, s0*s3*b, s1*s3*b, s2*s3*b, s3^2*b, s0*s4*b, s1*s4*b, s2*s4*b, s3*s4*b, s4^2*b, s0*s5*b, s1*s5*b, s2*s5*b, s3*s5*b, s4*s5*b, s5^2*b, s0*s6*b, s1*s6*b, s2*s6*b, s3*s6*b, s4*s6*b, s5*s6*b, s6^2*b, s0*s7*b, s1*s7*b, s2*s7*b, s3*s7*b, s4*s7*b, s5*s7*b, s6*s7*b, s7^2*b, s0*s8*b, s1*s8*b, s2*s8*b, s3*s8*b, s4*s8*b, s5*s8*b, s6*s8*b, s7*s8*b, s8^2*b, s0*s9*b, s1*s9*b, s2*s9*b, s3*s9*b, s4*s9*b, s5*s9*b, s6*s9*b, s7*s9*b, s8*s9*b, s9^2*b, s0*s10*b, s1*s10*b, s2*s10*b, s3*s10*b, s4*s10*b, s5*s10*b, s6*s10*b, s7*s10*b, s8*s10*b, s9*s10*b, s10^2*b, s0*s11*b, s1*s11*b, s2*s11*b, s3*s11*b, s4*s11*b, s5*s11*b, s6*s11*b, s7*s11*b, s8*s11*b, s9*s11*b, s10*s11*b, s11^2*b, s0*s12*b, s1*s12*b, s2*s12*b, s3*s12*b, s4*s12*b, s5*s12*b, s6*s12*b, s7*s12*b, s8*s12*b, s9*s12*b, s10*s12*b, s11*s12*b, s12^2*b, s0*s13*b, s1*s13*b, s2*s13*b, s3*s13*b, s4*s13*b, s5*s13*b, s6*s13*b, s7*s13*b, s8*s13*b, s9*s13*b, s10*s13*b, s11*s13*b, s12*s13*b, s13^2*b, s0*e*b, s1*e*b, s2*e*b, s3*e*b, s4*e*b, s5*e*b, s6*e*b, s7*e*b, s8*e*b, s9*e*b, s10*e*b, s11*e*b, s12*e*b, s13*e*b, e^2*b, s0*b^2, s1*b^2, s2*b^2, s3*b^2, s4*b^2, s5*b^2, s6*b^2, s7*b^2, s8*b^2, s9*b^2, s10*b^2, s11*b^2, s12*b^2, s13*b^2, e*b^2, b^3, s0^2, s0*s1, s1^2, s0*s2, s1*s2, s2^2, s0*s3, s1*s3, s2*s3, s3^2, s0*s4, s1*s4, s2*s4, s3*s4, s4^2, s0*s5, s1*s5, s2*s5, s3*s5, s4*s5, s5^2, s0*s6, s1*s6, s2*s6, s3*s6, s4*s6, s5*s6, s6^2, s0*s7, s1*s7, s2*s7, s3*s7, s4*s7, s5*s7, s6*s7, s7^2, s0*s8, s1*s8, s2*s8, s3*s8, s4*s8, s5*s8, s6*s8, s7*s8, s8^2, s0*s9, s1*s9, s2*s9, s3*s9, s4*s9, s5*s9, s6*s9, s7*s9, s8*s9, s9^2, s0*s10, s1*s10, s2*s10, s3*s10, s4*s10, s5*s10, s6*s10, s7*s10, s8*s10, s9*s10, s10^2, s0*s11, s1*s11, s2*s11, s3*s11, s4*s11, s5*s11, s6*s11, s7*s11, s8*s11, s9*s11, s10*s11, s11^2, s0*s12, s1*s12, s2*s12, s3*s12, s4*s12, s5*s12, s6*s12, s7*s12, s8*s12, s9*s12, s10*s12, s11*s12, s12^2, s0*s13, s1*s13, s2*s13, s3*s13, s4*s13, s5*s13, s6*s13, s7*s13, s8*s13, s9*s13, s10*s13, s11*s13, s12*s13, s13^2, s0*e, s1*e, s2*e, s3*e, s4*e, s5*e, s6*e, s7*e, s8*e, s9*e, s10*e, s11*e, s12*e, s13*e, e^2, s0*b, s1*b, s2*b, s3*b, s4*b, s5*b, s6*b, s7*b, s8*b, s9*b, s10*b, s11*b, s12*b, s13*b, e*b, b^2, s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, e, b, 1]

这边我们可以看到最后几项就包含了我们需要的secret，也就是向量s，同时我们还可以拿到b，有了s和b之后拿最后一组数据，再反向解出那组对应的向量(e0,e1,e2,e3)(e_0, e_1, e_2, e_3)​

这时候根据等式我们可以构造出如下的矩阵

L(s04s03∗s1⋮s0s1⋮s13eb)=R\begin{array}{l} L \begin{pmatrix} s_0 ^ 4 \\ s_0 ^ 3 * s_1 \\ \vdots \\ s_0 \\ s_1 \\ \vdots \\ s_{13} \\ e \\ b \end{pmatrix}= R \end{array}

这边的L中包含着每组等式对应项对应的系数，R是每个多项式对应的常数项移到等式右边也可以构成一个列向量

然后再进行一次迭代就拿到最后用于AES加密的seed，虽然顺序不确定，但是我们简单进行组合一下（去掉4次都是一样）即可拿到flag

完整exp：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
from Crypto.Util.number import long_to_bytes
from itertools import permutations
from Crypto.Cipher import AES
from ast import literal_eval
from gmpy2 import next_prime
from hashlib import md5
from tqdm import tqdm

with open('output.txt', 'r') as f:
    tmp = literal_eval(f.readline().split(' = ')[1].strip())
    a = tmp[0]
    AA = tmp[1::]
    BB = literal_eval(f.readline().split(' = ')[1].strip())[1::]
    C = f.readline().split(' = ')[1].strip()

d = 14
#先获取模数p
p = 0
for i in AA:
    if max(i) > p:
        p = max(i)
for i in BB:
    if max(i) > p:
        p = max(i)
for i in range(4):  #这边的话只要四次就可以得到p，本地测试的话十次以内就行
    p = next_prime(p)

#前面的运算只要x，只定义x运算会更快，之后拿到系数之后再用MY环来运算
PR.<x> = PolynomialRing(GF(p))
f = PR(list(b"DASCTF_XHLJ2025"))

#这是我们自己定义的
variables = [f's{i}' for i in range(14)] + ['e'] + ['b']
MY = PolynomialRing(GF(p), variables)
variables = MY.gens()
s = vector(variables[:14])
e = variables[-2]
b = variables[-1]

polys = []
for k in range(len(AA)):
    A = Matrix(GF(p), [(PR(AA[k])*x^i % f).list() for i in range(14)])
    for i in range(14):
        eq = (s * A.column(i) + e - BB[k][i]) ^ 4
        polys.append(eq)
    e = a * e + b

# print(len(polys))
# print(len(polys[0].monomials()))
# print(len(polys[d].monomials())) 
# print(polys[d].monomials())

L, R = [], []
for i in tqdm(polys[d::]):
    L.append(i.coefficients()[:-1])
    R.append(-i.coefficients()[-1])   #这边负号别忘记
L, R = Matrix(GF(p), L), vector(GF(p), R)
sol = (L.solve_right(R)).list()

#这边注意，因为常数已经被我们拿作向量R了，所以b应该是最后一项，s同理也要改变
b = sol[-1]
s = vector(sol[-2 - d:-2:])

seed = list(set((vector(BB[-1]) - s * Matrix(GF(p), [(PR(AA[-1])*x^i % f).list() for i in range(14)])).list()))
assert len(seed) == 4
tmp_seed = [(a * j + b) % p for j in seed]  #这边别忘记模p
secert = s.list()

for seed in tqdm(permutations(tmp_seed)):
    flag = AES.new(key=md5(str([b]+list(seed)+secret).encode()).digest(), nonce=b"Xenny.fans.club", mode=AES.MODE_CTR).decrypt(long_to_bytes(int(C, 16)))
    if flag.isascii():
        print(flag)  #b'DASCTF{jUsT_Lin34R1ZE_4nD_5OLv3_L1n3ar_SySt3m}'
        break

更新于：2025年2月25日

评论

评论区