-
Notifications
You must be signed in to change notification settings - Fork 0
/
polynomials.txt
33 lines (17 loc) · 13.1 KB
/
polynomials.txt
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
1) x1 - 3*x7*x12*x14*x15^2*x16^2 + 4*x7*x12*x14*x15^2*x16 + 3*x7*x12*x14*x15^2 + 4*x7*x12*x14*x15*x16^2 + x7*x12*x14*x15*x16 + 4*x7*x12*x14*x15 + 3*x7*x12*x14*x16^2 + 4*x7*x12*x14*x16 + x7*x12*x14 + 2*x7*x12*x15^2*x16^2 - 5*x7*x12*x15^2*x16 + 2*x7*x12*x15^2 - 5*x7*x12*x15*x16^2 - 3*x7*x12*x15*x16 + 2*x7*x12*x15 + 2*x7*x12*x16^2 + 2*x7*x12*x16 - 3*x7*x12 + 2*x7*x14*x15^2*x16^2 - 5*x7*x14*x15^2*x16 + 2*x7*x14*x15^2 - 5*x7*x14*x15*x16^2 - 3*x7*x14*x15*x16 + 2*x7*x14*x15 + 2*x7*x14*x16^2 + 2*x7*x14*x16 - 3*x7*x14 + 3*x7*x15^2*x16^2 + 4*x7*x15^2*x16 + x7*x15^2 + 4*x7*x15*x16^2 + 4*x7*x15*x16 + 5*x7*x15 + x7*x16^2 + 5*x7*x16 - x7 + 3*x8*x10*x12*x15^2*x16^2 - 4*x8*x10*x12*x15^2*x16 - 3*x8*x10*x12*x15^2 + 3*x8*x10*x12*x15*x16^3 + x8*x10*x12*x15*x16^2 - x8*x10*x12*x15*x16 - x8*x10*x12*x15 - 2*x8*x10*x12*x16^3 - 2*x8*x10*x12*x16^2 - 2*x8*x10*x15^2*x16^2 + 5*x8*x10*x15^2*x16 - 2*x8*x10*x15^2 - 2*x8*x10*x15*x16^3 - 5*x8*x10*x15*x16^2 - 4*x8*x10*x15*x16 - x8*x10*x15 - 3*x8*x10*x16^3 - 3*x8*x10*x16^2 - x8*x10*x16 + 4*x8*x10 + 3*x8*x12*x14*x15*x16^3 + 5*x8*x12*x14*x15*x16^2 + 2*x8*x12*x14*x15*x16 - 2*x8*x12*x14*x15 - 2*x8*x12*x14*x16^3 + 2*x8*x12*x14*x16^2 + 5*x8*x12*x14*x16 - x8*x12*x14 - 2*x8*x12*x15^2*x16^2 + 5*x8*x12*x15^2*x16 - 2*x8*x12*x15^2 - 4*x8*x12*x15*x16^3 - 3*x8*x12*x15*x16^2 + x8*x12*x15*x16 - 2*x8*x12*x15 + 5*x8*x12*x16^3 + 2*x8*x12*x16^2 - 4*x8*x12*x16 - 4*x8*x12 - 2*x8*x14*x15*x16^3 + 2*x8*x14*x15*x16^2 + 5*x8*x14*x15*x16 - x8*x14*x15 - 3*x8*x14*x16^3 + 5*x8*x14*x16^2 - 3*x8*x14*x16 + 3*x8*x14 - 3*x8*x15^2*x16^2 - 4*x8*x15^2*x16 - x8*x15^2 + 5*x8*x15*x16^3 + 5*x8*x15*x16 - x8*x15 - 4*x8*x16^3 - 5*x8*x16^2 - 2*x8*x16 + 2*x8 - 2*x10*x12*x15^2*x16^2 + 5*x10*x12*x15^2*x16 - 2*x10*x12*x15^2 - 2*x10*x12*x15*x16^3 - 5*x10*x12*x15*x16^2 - 4*x10*x12*x15*x16 - x10*x12*x15 - 3*x10*x12*x16^3 - 3*x10*x12*x16^2 - x10*x12*x16 + 4*x10*x12 - 3*x10*x15^2*x16^2 - 4*x10*x15^2*x16 - x10*x15^2 - 3*x10*x15*x16^3 - 5*x10*x15*x16^2 - 3*x10*x15*x16 - 4*x10*x15 - 2*x10*x16^3 - 2*x10*x16^2 + x10 + 2*x12*x14*x15^2*x16^2 - 5*x12*x14*x15^2*x16 + 2*x12*x14*x15^2 - 2*x12*x14*x15*x16^3 - 3*x12*x14*x15*x16^2 + 2*x12*x14*x15*x16 + x12*x14*x15 - 3*x12*x14*x16^3 - 4*x12*x14*x16^2 - x12*x14*x16 + 5*x12*x15*x16^3 + 4*x12*x15*x16^2 - 2*x12*x15*x16 + 4*x12*x15 - 4*x12*x16^3 - 4*x12*x16^2 + 3*x12*x16 + 2*x12 + 3*x14*x15^2*x16^2 + 4*x14*x15^2*x16 + x14*x15^2 - 3*x14*x15*x16^3 - 2*x14*x15*x16^2 + x14*x15*x16 - 3*x14*x15 - 2*x14*x16^3 - 2*x14*x16^2 + 3*x14*x16 - 4*x15*x16^3 - 4*x15*x16^2 + 3*x15*x16 + 2*x15 - 2*x16^3 + 5*x16^2 + 5*x16 + 3,
2) x2 + 3*x7*x12*x14*x15^2*x16^2 - 4*x7*x12*x14*x15^2*x16 - 3*x7*x12*x14*x15^2 - 4*x7*x12*x14*x15*x16^2 - x7*x12*x14*x15*x16 - 4*x7*x12*x14*x15 - 3*x7*x12*x14*x16^2 - 4*x7*x12*x14*x16 - x7*x12*x14 - 2*x7*x12*x15^2*x16^2 + 5*x7*x12*x15^2*x16 - 2*x7*x12*x15^2 + 5*x7*x12*x15*x16^2 + 3*x7*x12*x15*x16 - 2*x7*x12*x15 - 2*x7*x12*x16^2 - 2*x7*x12*x16 + 3*x7*x12 - 2*x7*x14*x15^2*x16^2 + 5*x7*x14*x15^2*x16 - 2*x7*x14*x15^2 + 5*x7*x14*x15*x16^2 + 3*x7*x14*x15*x16 - 2*x7*x14*x15 - 2*x7*x14*x16^2 - 2*x7*x14*x16 + 3*x7*x14 - 3*x7*x15^2*x16^2 - 4*x7*x15^2*x16 - x7*x15^2 - 4*x7*x15*x16^2 - 4*x7*x15*x16 - 5*x7*x15 - x7*x16^2 - 5*x7*x16 - 3*x8*x10*x12*x15^2*x16^2 + 4*x8*x10*x12*x15^2*x16 + 3*x8*x10*x12*x15^2 - 3*x8*x10*x12*x15*x16^3 - x8*x10*x12*x15*x16^2 + x8*x10*x12*x15*x16 + x8*x10*x12*x15 + 2*x8*x10*x12*x16^3 + 2*x8*x10*x12*x16^2 + 2*x8*x10*x15^2*x16^2 - 5*x8*x10*x15^2*x16 + 2*x8*x10*x15^2 + 2*x8*x10*x15*x16^3 + 5*x8*x10*x15*x16^2 + 4*x8*x10*x15*x16 + x8*x10*x15 + 3*x8*x10*x16^3 + 3*x8*x10*x16^2 + x8*x10*x16 - 4*x8*x10 - 3*x8*x12*x14*x15*x16^3 - 5*x8*x12*x14*x15*x16^2 - 2*x8*x12*x14*x15*x16 + 2*x8*x12*x14*x15 + 2*x8*x12*x14*x16^3 - 2*x8*x12*x14*x16^2 - 5*x8*x12*x14*x16 + x8*x12*x14 + 2*x8*x12*x15^2*x16^2 - 5*x8*x12*x15^2*x16 + 2*x8*x12*x15^2 + 4*x8*x12*x15*x16^3 + 3*x8*x12*x15*x16^2 - x8*x12*x15*x16 + 2*x8*x12*x15 - 5*x8*x12*x16^3 - 2*x8*x12*x16^2 + 4*x8*x12*x16 + 4*x8*x12 + 2*x8*x14*x15*x16^3 - 2*x8*x14*x15*x16^2 - 5*x8*x14*x15*x16 + x8*x14*x15 + 3*x8*x14*x16^3 - 5*x8*x14*x16^2 + 3*x8*x14*x16 - 3*x8*x14 + 3*x8*x15^2*x16^2 + 4*x8*x15^2*x16 + x8*x15^2 - 5*x8*x15*x16^3 - 5*x8*x15*x16 + x8*x15 + 4*x8*x16^3 + 5*x8*x16^2 + 2*x8*x16 - 3*x8 + 2*x10*x12*x15^2*x16^2 - 5*x10*x12*x15^2*x16 + 2*x10*x12*x15^2 + 2*x10*x12*x15*x16^3 + 5*x10*x12*x15*x16^2 + 4*x10*x12*x15*x16 + x10*x12*x15 + 3*x10*x12*x16^3 + 3*x10*x12*x16^2 + x10*x12*x16 - 4*x10*x12 + 3*x10*x15^2*x16^2 + 4*x10*x15^2*x16 + x10*x15^2 + 3*x10*x15*x16^3 + 5*x10*x15*x16^2 + 3*x10*x15*x16 + 4*x10*x15 + 2*x10*x16^3 + 2*x10*x16^2 - x10 - 2*x12*x14*x15^2*x16^2 + 5*x12*x14*x15^2*x16 - 2*x12*x14*x15^2 + 2*x12*x14*x15*x16^3 + 3*x12*x14*x15*x16^2 - 2*x12*x14*x15*x16 - x12*x14*x15 + 3*x12*x14*x16^3 + 4*x12*x14*x16^2 + x12*x14*x16 - 5*x12*x15*x16^3 - 4*x12*x15*x16^2 + 2*x12*x15*x16 - 4*x12*x15 + 4*x12*x16^3 + 4*x12*x16^2 - 3*x12*x16 - 2*x12 - 3*x14*x15^2*x16^2 - 4*x14*x15^2*x16 - x14*x15^2 + 3*x14*x15*x16^3 + 2*x14*x15*x16^2 - x14*x15*x16 + 3*x14*x15 + 2*x14*x16^3 + 2*x14*x16^2 - 3*x14*x16 + 4*x15*x16^3 + 4*x15*x16^2 - 3*x15*x16 - 2*x15 + 2*x16^3 - 5*x16^2 - 5*x16 - 3,
3) x3 + x7 - x12 - x16,
4) x4 + x8 + x12 + x16 + 1,
5) x5 + 3*x7*x12*x14*x15^2*x16^2 - 4*x7*x12*x14*x15^2*x16 - 3*x7*x12*x14*x15^2 - 4*x7*x12*x14*x15*x16^2 - x7*x12*x14*x15*x16 - 4*x7*x12*x14*x15 - 3*x7*x12*x14*x16^2 - 4*x7*x12*x14*x16 - x7*x12*x14 - 2*x7*x12*x15^2*x16^2 + 5*x7*x12*x15^2*x16 - 2*x7*x12*x15^2 + 5*x7*x12*x15*x16^2 + 3*x7*x12*x15*x16 - 2*x7*x12*x15 - 2*x7*x12*x16^2 - 2*x7*x12*x16 + 3*x7*x12 - 2*x7*x14*x15^2*x16^2 + 5*x7*x14*x15^2*x16 - 2*x7*x14*x15^2 + 5*x7*x14*x15*x16^2 + 3*x7*x14*x15*x16 - 2*x7*x14*x15 - 2*x7*x14*x16^2 - 2*x7*x14*x16 + 3*x7*x14 - 3*x7*x15^2*x16^2 - 4*x7*x15^2*x16 - x7*x15^2 - 4*x7*x15*x16^2 - 4*x7*x15*x16 - 5*x7*x15 - x7*x16^2 - 5*x7*x16 + x7 - 3*x8*x10*x12*x15^2*x16^2 + 4*x8*x10*x12*x15^2*x16 + 3*x8*x10*x12*x15^2 - 3*x8*x10*x12*x15*x16^3 - x8*x10*x12*x15*x16^2 + x8*x10*x12*x15*x16 + x8*x10*x12*x15 + 2*x8*x10*x12*x16^3 + 2*x8*x10*x12*x16^2 + 2*x8*x10*x15^2*x16^2 - 5*x8*x10*x15^2*x16 + 2*x8*x10*x15^2 + 2*x8*x10*x15*x16^3 + 5*x8*x10*x15*x16^2 + 4*x8*x10*x15*x16 + x8*x10*x15 + 3*x8*x10*x16^3 + 3*x8*x10*x16^2 + x8*x10*x16 - 4*x8*x10 - 3*x8*x12*x14*x15*x16^3 - 5*x8*x12*x14*x15*x16^2 - 2*x8*x12*x14*x15*x16 + 2*x8*x12*x14*x15 + 2*x8*x12*x14*x16^3 - 2*x8*x12*x14*x16^2 - 5*x8*x12*x14*x16 + x8*x12*x14 + 2*x8*x12*x15^2*x16^2 - 5*x8*x12*x15^2*x16 + 2*x8*x12*x15^2 + 4*x8*x12*x15*x16^3 + 3*x8*x12*x15*x16^2 - x8*x12*x15*x16 + 2*x8*x12*x15 - 5*x8*x12*x16^3 - 2*x8*x12*x16^2 + 4*x8*x12*x16 + 4*x8*x12 + 2*x8*x14*x15*x16^3 - 2*x8*x14*x15*x16^2 - 5*x8*x14*x15*x16 + x8*x14*x15 + 3*x8*x14*x16^3 - 5*x8*x14*x16^2 + 3*x8*x14*x16 - 3*x8*x14 + 3*x8*x15^2*x16^2 + 4*x8*x15^2*x16 + x8*x15^2 - 5*x8*x15*x16^3 - 5*x8*x15*x16 + x8*x15 + 4*x8*x16^3 + 5*x8*x16^2 + 2*x8*x16 - 2*x8 + 2*x10*x12*x15^2*x16^2 - 5*x10*x12*x15^2*x16 + 2*x10*x12*x15^2 + 2*x10*x12*x15*x16^3 + 5*x10*x12*x15*x16^2 + 4*x10*x12*x15*x16 + x10*x12*x15 + 3*x10*x12*x16^3 + 3*x10*x12*x16^2 + x10*x12*x16 - 4*x10*x12 + 3*x10*x15^2*x16^2 + 4*x10*x15^2*x16 + x10*x15^2 + 3*x10*x15*x16^3 + 5*x10*x15*x16^2 + 3*x10*x15*x16 + 4*x10*x15 + 2*x10*x16^3 + 2*x10*x16^2 - 2*x10 - 2*x12*x14*x15^2*x16^2 + 5*x12*x14*x15^2*x16 - 2*x12*x14*x15^2 + 2*x12*x14*x15*x16^3 + 3*x12*x14*x15*x16^2 - 2*x12*x14*x15*x16 - x12*x14*x15 + 3*x12*x14*x16^3 + 4*x12*x14*x16^2 + x12*x14*x16 - 5*x12*x15*x16^3 - 4*x12*x15*x16^2 + 2*x12*x15*x16 - 4*x12*x15 + 4*x12*x16^3 + 4*x12*x16^2 - 3*x12*x16 - 2*x12 - 3*x14*x15^2*x16^2 - 4*x14*x15^2*x16 - x14*x15^2 + 3*x14*x15*x16^3 + 2*x14*x15*x16^2 - x14*x15*x16 + 3*x14*x15 + 2*x14*x16^3 + 2*x14*x16^2 - 3*x14*x16 - x14 + 4*x15*x16^3 + 4*x15*x16^2 - 3*x15*x16 - 2*x15 + 2*x16^3 - 5*x16^2 - 5*x16 - 3,
6) x6 - 3*x7*x12*x14*x15^2*x16^2 + 4*x7*x12*x14*x15^2*x16 + 3*x7*x12*x14*x15^2 + 4*x7*x12*x14*x15*x16^2 + x7*x12*x14*x15*x16 + 4*x7*x12*x14*x15 + 3*x7*x12*x14*x16^2 + 4*x7*x12*x14*x16 + x7*x12*x14 + 2*x7*x12*x15^2*x16^2 - 5*x7*x12*x15^2*x16 + 2*x7*x12*x15^2 - 5*x7*x12*x15*x16^2 - 3*x7*x12*x15*x16 + 2*x7*x12*x15 + 2*x7*x12*x16^2 + 2*x7*x12*x16 - 3*x7*x12 + 2*x7*x14*x15^2*x16^2 - 5*x7*x14*x15^2*x16 + 2*x7*x14*x15^2 - 5*x7*x14*x15*x16^2 - 3*x7*x14*x15*x16 + 2*x7*x14*x15 + 2*x7*x14*x16^2 + 2*x7*x14*x16 - 3*x7*x14 + 3*x7*x15^2*x16^2 + 4*x7*x15^2*x16 + x7*x15^2 + 4*x7*x15*x16^2 + 4*x7*x15*x16 + 5*x7*x15 + x7*x16^2 + 5*x7*x16 + 3*x8*x10*x12*x15^2*x16^2 - 4*x8*x10*x12*x15^2*x16 - 3*x8*x10*x12*x15^2 + 3*x8*x10*x12*x15*x16^3 + x8*x10*x12*x15*x16^2 - x8*x10*x12*x15*x16 - x8*x10*x12*x15 - 2*x8*x10*x12*x16^3 - 2*x8*x10*x12*x16^2 - 2*x8*x10*x15^2*x16^2 + 5*x8*x10*x15^2*x16 - 2*x8*x10*x15^2 - 2*x8*x10*x15*x16^3 - 5*x8*x10*x15*x16^2 - 4*x8*x10*x15*x16 - x8*x10*x15 - 3*x8*x10*x16^3 - 3*x8*x10*x16^2 - x8*x10*x16 + 4*x8*x10 + 3*x8*x12*x14*x15*x16^3 + 5*x8*x12*x14*x15*x16^2 + 2*x8*x12*x14*x15*x16 - 2*x8*x12*x14*x15 - 2*x8*x12*x14*x16^3 + 2*x8*x12*x14*x16^2 + 5*x8*x12*x14*x16 - x8*x12*x14 - 2*x8*x12*x15^2*x16^2 + 5*x8*x12*x15^2*x16 - 2*x8*x12*x15^2 - 4*x8*x12*x15*x16^3 - 3*x8*x12*x15*x16^2 + x8*x12*x15*x16 - 2*x8*x12*x15 + 5*x8*x12*x16^3 + 2*x8*x12*x16^2 - 4*x8*x12*x16 - 4*x8*x12 - 2*x8*x14*x15*x16^3 + 2*x8*x14*x15*x16^2 + 5*x8*x14*x15*x16 - x8*x14*x15 - 3*x8*x14*x16^3 + 5*x8*x14*x16^2 - 3*x8*x14*x16 + 3*x8*x14 - 3*x8*x15^2*x16^2 - 4*x8*x15^2*x16 - x8*x15^2 + 5*x8*x15*x16^3 + 5*x8*x15*x16 - x8*x15 - 4*x8*x16^3 - 5*x8*x16^2 - 2*x8*x16 + 3*x8 - 2*x10*x12*x15^2*x16^2 + 5*x10*x12*x15^2*x16 - 2*x10*x12*x15^2 - 2*x10*x12*x15*x16^3 - 5*x10*x12*x15*x16^2 - 4*x10*x12*x15*x16 - x10*x12*x15 - 3*x10*x12*x16^3 - 3*x10*x12*x16^2 - x10*x12*x16 + 4*x10*x12 - 3*x10*x15^2*x16^2 - 4*x10*x15^2*x16 - x10*x15^2 - 3*x10*x15*x16^3 - 5*x10*x15*x16^2 - 3*x10*x15*x16 - 4*x10*x15 - 2*x10*x16^3 - 2*x10*x16^2 + 2*x10 + 2*x12*x14*x15^2*x16^2 - 5*x12*x14*x15^2*x16 + 2*x12*x14*x15^2 - 2*x12*x14*x15*x16^3 - 3*x12*x14*x15*x16^2 + 2*x12*x14*x15*x16 + x12*x14*x15 - 3*x12*x14*x16^3 - 4*x12*x14*x16^2 - x12*x14*x16 + 5*x12*x15*x16^3 + 4*x12*x15*x16^2 - 2*x12*x15*x16 + 4*x12*x15 - 4*x12*x16^3 - 4*x12*x16^2 + 3*x12*x16 + 2*x12 + 3*x14*x15^2*x16^2 + 4*x14*x15^2*x16 + x14*x15^2 - 3*x14*x15*x16^3 - 2*x14*x15*x16^2 + x14*x15*x16 - 3*x14*x15 - 2*x14*x16^3 - 2*x14*x16^2 + 3*x14*x16 + x14 - 4*x15*x16^3 - 4*x15*x16^2 + 3*x15*x16 + 2*x15 - 2*x16^3 + 5*x16^2 + 5*x16 + 4,
7) x7^2 - x7*x12 - x7*x16 + x12*x16,
8) x7*x10 + 5*x7*x12*x14*x15^2*x16^3 + x7*x12*x14*x15^2*x16^2 - 2*x7*x12*x14*x15^2*x16 - x7*x12*x14*x15^2 - 3*x7*x12*x14*x15*x16^3 + 5*x7*x12*x14*x15*x16^2 + 4*x7*x12*x14*x15*x16 - 5*x7*x12*x14*x16^3 - 4*x7*x12*x14*x16^2 + 2*x7*x12*x14*x16 - 4*x7*x12*x14 + 4*x7*x12*x15^2*x16^3 - 3*x7*x12*x15^2*x16^2 + 2*x7*x12*x15^2*x16 + x7*x12*x15*x16^3 + 3*x7*x12*x15*x16^2 + 4*x7*x12*x15*x16 + 3*x7*x12*x15 + 4*x7*x12*x16^3 + 4*x7*x12*x16^2 - 3*x7*x12*x16 - 2*x7*x12 + 4*x7*x14*x15^2*x16^3 - 3*x7*x14*x15^2*x16^2 + 2*x7*x14*x15^2*x16 + x7*x14*x15*x16^3 + 3*x7*x14*x15*x16^2 + 4*x7*x14*x15*x16 + 3*x7*x14*x15 + 4*x7*x14*x16^3 + 4*x7*x14*x16^2 - 3*x7*x14*x16 - 2*x7*x14 - 5*x7*x15^2*x16^3 - 4*x7*x15^2*x16^2 + 2*x7*x15^2*x16 - 4*x7*x15^2 - 3*x7*x15*x16^3 - 3*x7*x15*x16^2 + 5*x7*x15*x16 - 4*x7*x15 + 2*x7*x16^3 - 5*x7*x16^2 - 5*x7*x16 - 3*x7 - 5*x8*x10*x12*x15^2*x16^3 - x8*x10*x12*x15^2*x16^2 + 2*x8*x10*x12*x15^2*x16 + x8*x10*x12*x15^2 + 3*x8*x10*x12*x15*x16^3 - 3*x8*x10*x12*x15*x16^2 - 3*x8*x10*x12*x15*x16 + 4*x8*x10*x12*x16^3 + x8*x10*x12*x16^2 - 4*x8*x10*x15^2*x16^3 + 3*x8*x10*x15^2*x16^2 - 2*x8*x10*x15^2*x16 - 2*x8*x10*x15*x16^3 + 5*x8*x10*x15*x16^2 - 2*x8*x10*x15*x16 + 4*x8*x10*x15 + x8*x10*x16^3 + 4*x8*x10*x16 + 2*x8*x10 + 4*x8*x12*x14*x15*x16^2 + 2*x8*x12*x14*x15*x16 - x8*x12*x14*x15 + x8*x12*x14*x16^3 - x8*x12*x14*x16^2 - 4*x8*x12*x14*x16 + x8*x12*x14 - 4*x8*x12*x15^2*x16^3 + 3*x8*x12*x15^2*x16^2 - 2*x8*x12*x15^2*x16 - x8*x12*x15*x16^3 + 4*x8*x12*x15*x16^2 + 5*x8*x12*x15*x16 + 5*x8*x12*x15 - 4*x8*x12*x16^3 - 5*x8*x12*x16^2 - 3*x8*x12*x16 + 4*x8*x12 + x8*x14*x15*x16^3 - x8*x14*x15*x16^2 - 4*x8*x14*x15*x16 + x8*x14*x15 - 5*x8*x14*x16^3 - 5*x8*x14*x16^2 + 4*x8*x14*x16 + 3*x8*x14 + 5*x8*x15^2*x16^3 + 4*x8*x15^2*x16^2 - 2*x8*x15^2*x16 + 4*x8*x15^2 + 3*x8*x15*x16^3 + 2*x8*x15*x16^2 - 5*x8*x15 - 2*x8*x16^3 + 2*x8*x16^2 - 2*x8*x16 + 4*x8 - 4*x10*x12*x15^2*x16^3 + 3*x10*x12*x15^2*x16^2 - 2*x10*x12*x15^2*x16 - 2*x10*x12*x15*x16^3 + 5*x10*x12*x15*x16^2 - 2*x10*x12*x15*x16 + 4*x10*x12*x15 + x10*x12*x16^3 + 4*x10*x12*x16 + x10*x12 + 5*x10*x15^2*x16^3 + 4*x10*x15^2*x16^2 - 2*x10*x15^2*x16 + 4*x10*x15^2 - 3*x10*x15*x16^3 - 4*x10*x15*x16^2 - 4*x10*x15*x16 + 3*x10*x15 - 3*x10*x16^2 + 4*x10*x16 + 4*x10 + 4*x12*x14*x15^2*x16^3 - 3*x12*x14*x15^2*x16^2 + 2*x12*x14*x15^2*x16 + 2*x12*x14*x15*x16^3 + 2*x12*x14*x15*x16^2 + 4*x12*x14*x15 - x12*x14*x16^3 - x12*x14*x16^2 + x12*x14*x16 + x12*x14 - x12*x15*x16^2 + 5*x12*x15*x16 + 3*x12*x15 - 3*x12*x16^2 + 5*x12*x16 + x12 - 5*x14*x15^2*x16^3 - 4*x14*x15^2*x16^2 + 2*x14*x15^2*x16 - 4*x14*x15^2 + 3*x14*x15*x16^3 + 3*x14*x15*x16^2 - 2*x14*x15*x16 - x14*x15 - 3*x14 - 3*x15*x16^2 + 5*x15*x16 + x15 + 3*x16^2 + 2*x16 - 5,
9) x8^2 + x8*x12 + x8*x16 + x8 - x12*x15 - x15^2 - x15*x16 - x15,
10) x9 + x10 - x15 - x16,
11) x10^2 - x10*x15 - x10*x16 + x15*x16,
12) x11 + x12 + x15 + x16 + 1,
13) x12^2 + x12*x15 + x12*x16 + x12 + x15^2 + x15*x16 + x15 + x16^2 + x16 + 2,
14) x13 + x14 + x15 + x16 + 1,
15) x14^2 + x14*x15 + x14*x16 + x14 + x15^2 + x15*x16 + x15 + x16^2 + x16 + 2,
16) x15^3 + x15^2*x16 + x15^2 + x15*x16^2 + x15*x16 + 2*x15 + x16^3 + x16^2 + 2*x16 + 5,
17) x16^4 + x16^3 + 2*x16^2 + 5*x16 + 2