Problem v1l1o57


Unknowns | Inequalities | Equations | Solution 1 | Solution 2 | Computing time

Unknowns

All solutions for the following 33 unknowns have to be determined:
a1, ..., a9, b1, ..., b24 

Inequalities

Each of the following lists represents one inequality which states that not all unknowns in this list may vanish. These inequalities filter out solutions which are trivial for the application.
{a1}, {a2,a3,a4,a5,a6,a7,a8,a9}, {b1}

Equations

All comma separated 198 expressions involving 3125 terms have to vanish. All terms are products of one a- and one b-unknown.
5*a1*b2 - 7*a2*b1,
5*a1*b13 - 7*a7*b1,
2*a8*b24 - 3*a9*b23,
5*a1*b14 - a2*b2 - 7*a8*b1,
20*a1*b2 + 5*a1*b3 - 42*a2*b1 - 7*a3*b1,
5*a1*b10 + 10*a1*b13 - 7*a5*b1 - 21*a7*b1,
10*a1*b11 + 5*a1*b12 - 35*a6*b1 - 21*a7*b1,
5*a1*b12 + 10*a1*b13 - 7*a6*b1 - 21*a7*b1,
15*a1*b23 + 3*a2*b14 - 10*a8*b2 - a9*b2,
9*a2*b23 + a2*b24 - 6*a8*b14 - 2*a9*b14,
15*a1*b11 + 10*a1*b12 + 5*a1*b13 - 56*a6*b1 - 42*a7*b1,
5*a1*b11 + 10*a1*b12 + 10*a1*b13 - 28*a6*b1 - 35*a7*b1,
20*a1*b2 + 10*a1*b3 + 5*a1*b5 - 70*a2*b1 - 21*a3*b1 - 7*a5*b1,
10*a1*b10 + 10*a1*b13 + 5*a1*b7 - 7*a3*b1 - 21*a5*b1 - 35*a7*b1,
5*a1*b10 + 5*a1*b12 + 20*a1*b13 - 7*a5*b1 - 7*a6*b1 - 42*a7*b1,
40*a1*b14 + 5*a1*b15 - 4*a2*b3 + 2*a3*b2 - 84*a8*b1 - 7*a9*b1,
5*a1*b21 + 3*a2*b13 + a5*b13 - a7*b10 - 5*a7*b2 - 7*a9*b1,
18*a2*b23 + 3*a2*b24 + a3*b24 - 12*a8*b14 - 3*a9*b14 - a9*b15,
3*a2*b24 + a5*b24 - 6*a7*b23 + 4*a8*b21 - 3*a9*b14 - a9*b17,
3*a2*b24 - a6*b24 + 3*a7*b24 - 3*a9*b14 + a9*b19 - 3*a9*b21,
40*a1*b14 + 5*a1*b15 - 14*a2*b2 + 3*a2*b3 - 5*a3*b2 - 84*a8*b1 - 7*a9*b1,
5*a1*b21 + 3*a2*b13 - a6*b13 + a7*b12 - 2*a7*b13 - 5*a7*b2 - 7*a9*b1,
60*a1*b24 + a6*b16 + a6*b18 + a6*b20 - 12*a8*b12 - 12*a9*b12 - 3*a9*b4,
2*a3*b24 + 2*a6*b24 + 12*a7*b23 + 6*a7*b24 - 2*a8*b22 - a9*b20 - a9*b22,
60*a1*b2 + 30*a1*b3 + 10*a1*b4 + 5*a1*b5 - 210*a2*b1 - 63*a3*b1 - 14*a4*b1 - 7*
a5*b1,
10*a1*b2 + 10*a1*b3 + 10*a1*b5 + 5*a1*b7 - 70*a2*b1 - 35*a3*b1 - 21*a5*b1 - 7*
a7*b1,
5*a1*b10 + 5*a1*b3 + 10*a1*b5 + 10*a1*b7 - 42*a2*b1 - 35*a3*b1 - 35*a5*b1 - 21*
a7*b1,
10*a1*b10 + 5*a1*b13 + 5*a1*b5 + 10*a1*b7 - 14*a2*b1 - 21*a3*b1 - 35*a5*b1 - 35
*a7*b1,
60*a1*b23 + 5*a1*b24 + 6*a2*b14 + 3*a2*b15 - 3*a3*b14 - 40*a8*b2 - 5*a9*b2 - a9
*b3,
5*a1*b24 + 3*a2*b21 + a5*b21 - 3*a7*b14 - a7*b17 + 4*a8*b13 - a9*b10 - 5*a9*b2,
10*a1*b24 + 3*a2*b19 - 3*a6*b14 - 3*a6*b21 + 3*a7*b19 + a9*b11 - 10*a9*b13 - 10
*a9*b2,
5*a1*b24 + 3*a2*b21 - a6*b21 - 3*a7*b14 + a7*b19 + a9*b12 - 5*a9*b13 - 5*a9*b2,
12*a2*b23 + 2*a2*b24 + 3*a3*b23 + a3*b24 - 4*a8*b14 - 2*a8*b15 - a9*b14 - a9*
b15,
18*a2*b23 + 9*a2*b24 + 3*a5*b24 - 6*a6*b23 - 12*a8*b14 + 4*a8*b19 - 9*a9*b14 - 
3*a9*b17,
6*a2*b24 + 3*a6*b23 + a6*b24 + 6*a7*b24 - 2*a8*b19 - 3*a9*b14 - a9*b19 - 3*a9*
b21,
10*a1*b10 + 5*a1*b11 + 20*a1*b12 + 30*a1*b13 + 5*a1*b9 - 14*a4*b1 - 21*a5*b1 - 
49*a6*b1 - 105*a7*b1,
120*a1*b14 + 30*a1*b15 + 5*a1*b17 + 5*a1*b18 - 6*a2*b3 - 3*a2*b5 - a3*b3 - 420*
a8*b1 - 63*a9*b1,
120*a1*b14 + 60*a1*b15 + 20*a1*b16 + 20*a1*b18 + 5*a1*b20 - 6*a2*b4 - 3*a3*b4 -
 840*a8*b1 - 210*a9*b1,
30*a1*b19 + 60*a1*b20 + 30*a1*b22 - 3*a3*b11 - 6*a4*b11 - 3*a5*b11 - 3*a6*b11 +
 a6*b6 - 630*a9*b1,
10*a1*b21 - 10*a2*b13 - a5*b13 + a6*b13 + a7*b10 - a7*b12 - 2*a7*b13 + 6*a7*b2 
- 14*a9*b1,
120*a1*b23 + 10*a1*b24 + 12*a2*b14 + a2*b15 + 4*a3*b14 - 40*a8*b2 - 10*a8*b3 - 
5*a9*b2 - 2*a9*b3,
120*a1*b23 + 20*a1*b24 + 2*a3*b14 + a3*b15 - 12*a8*b3 - 2*a8*b5 - 2*a9*b3 - a9*
b4 - a9*b5,
30*a1*b2 + 30*a1*b3 + 20*a1*b4 + 10*a1*b5 + 5*a1*b6 - 210*a2*b1 - 105*a3*b1 - 
42*a4*b1 - 21*a5*b1 - 7*a6*b1,
20*a1*b10 + 10*a1*b12 + 30*a1*b13 + 5*a1*b7 + 5*a1*b9 - 7*a3*b1 - 14*a4*b1 - 42
*a5*b1 - 21*a6*b1 - 105*a7*b1,
5*a1*b10 + 50*a1*b11 + 25*a1*b12 + 5*a1*b13 + 20*a1*b8 + 15*a1*b9 - 70*a4*b1 - 
56*a5*b1 - 245*a6*b1 - 147*a7*b1,
10*a1*b10 + 25*a1*b11 + 30*a1*b12 + 20*a1*b13 + 10*a1*b8 + 10*a1*b9 - 42*a4*b1 
- 42*a5*b1 - 147*a6*b1 - 147*a7*b1,
120*a1*b14 + 30*a1*b15 + 5*a1*b16 + 5*a1*b18 - 6*a2*b3 - 3*a2*b4 + a3*b2 - a3*
b3 - 420*a8*b1 - 63*a9*b1,
120*a1*b14 + 60*a1*b15 + 20*a1*b17 + 20*a1*b18 + 5*a1*b22 - 6*a2*b5 - a3*b3 - 3
*a3*b5 - 840*a8*b1 - 210*a9*b1,
5*a1*b17 + 10*a1*b21 + 3*a2*b10 + 3*a2*b13 + a3*b13 - 5*a5*b2 - 10*a7*b2 - a7*
b7 - 28*a8*b1 - 21*a9*b1,
10*a1*b19 + 5*a1*b21 + 3*a2*b11 - 10*a6*b13 - 10*a6*b2 + 3*a7*b11 + a7*b12 - 5*
a7*b13 - 5*a7*b2 - 35*a9*b1,
10*a2*b24 - a5*b24 + a6*b24 + 24*a7*b23 + 15*a7*b24 - 16*a8*b21 - 2*a9*b14 + a9
*b17 - a9*b19 - 9*a9*b21,
12*a2*b24 - a3*b24 + a6*b24 + 18*a7*b23 + 15*a7*b24 - 12*a8*b21 - 6*a9*b14 + a9
*b15 - a9*b19 - 9*a9*b21,
40*a1*b14 + 10*a1*b15 + 5*a1*b17 - 20*a2*b2 + 3*a2*b3 + 3*a2*b5 - 10*a3*b2 - 5*
a5*b2 - 2*a7*b2 - 140*a8*b1 - 21*a9*b1,
15*a1*b19 + 10*a1*b21 + 3*a2*b11 + 3*a2*b12 - 15*a6*b13 - 15*a6*b2 + 4*a7*b11 +
 3*a7*b12 - 10*a7*b13 - 10*a7*b2 - 56*a9*b1,
5*a1*b19 + 10*a1*b21 + 3*a2*b12 + 3*a2*b13 - 6*a6*b13 - 5*a6*b2 + a7*b11 + 3*a7
*b12 - 7*a7*b13 - 10*a7*b2 - 28*a9*b1,
20*a1*b21 + 5*a1*b22 - 20*a2*b13 - 5*a3*b13 - a5*b12 + a6*b10 + 2*a6*b13 - 4*a7
*b12 + 6*a7*b2 + 3*a7*b3 - 56*a9*b1,
10*a1*b21 + 10*a1*b22 - 10*a2*b13 - 10*a3*b13 - 10*a5*b13 - a7*b12 - 5*a7*b13 +
 a7*b3 + 3*a7*b5 + 3*a7*b7 - 70*a9*b1,
60*a1*b23 + 10*a1*b24 + 3*a2*b15 + 3*a2*b17 + 2*a2*b21 - 3*a3*b14 - 3*a5*b14 - 
4*a7*b14 - 40*a8*b2 - 10*a9*b2 - a9*b5,
30*a1*b23 + 10*a1*b24 + 3*a2*b17 + 3*a2*b21 + a3*b21 - 3*a5*b14 - 3*a7*b14 - a7
*b15 - 20*a8*b2 - 10*a9*b2 - a9*b7,
15*a1*b24 + 3*a2*b19 + 3*a2*b21 - 3*a6*b14 - 4*a6*b21 - 3*a7*b14 + 4*a7*b19 + 
a9*b11 + a9*b12 - 15*a9*b13 - 15*a9*b2,
120*a1*b24 - a3*b22 + a6*b22 + 6*a7*b15 + 6*a7*b17 + 6*a7*b18 + 3*a7*b22 - 120*
a8*b13 - 6*a9*b11 - 60*a9*b13 - 6*a9*b5,
40*a1*b2 + 40*a1*b3 + 20*a1*b4 + 20*a1*b5 + 5*a1*b6 + 5*a1*b7 - 280*a2*b1 - 140
*a3*b1 - 42*a4*b1 - 42*a5*b1 - 7*a6*b1 - 7*a7*b1,
a1*b10 + 6*a1*b11 + 2*a1*b12 + 2*a1*b6 + a1*b7 + 6*a1*b8 + 4*a1*b9 - 7*a3*b1 - 
28*a4*b1 - 21*a5*b1 - 42*a6*b1 - 21*a7*b1,
5*a1*b15 + 10*a1*b17 + 10*a1*b21 + 3*a2*b10 + 2*a2*b13 + 3*a2*b7 - 5*a3*b2 - 10
*a5*b2 - 10*a7*b2 - a7*b5 - 84*a8*b1 - 35*a9*b1,
20*a1*b15 + 40*a1*b17 + 30*a1*b18 + 20*a1*b21 + 30*a1*b22 - 2*a2*b7 + a3*b5 - 3
*a3*b7 - 5*a5*b7 - 2*a7*b7 - 560*a8*b1 - 420*a9*b1,
20*a1*b24 - a5*b21 + a6*b21 + 12*a7*b14 + a7*b17 - a7*b19 + 6*a7*b21 - 24*a8*
b13 + a9*b10 - a9*b12 - 15*a9*b13 - 8*a9*b2,
24*a2*b24 - a3*b24 + 6*a6*b23 + 3*a6*b24 + 18*a7*b23 + 27*a7*b24 - 4*a8*b19 - 
12*a8*b21 - 12*a9*b14 + a9*b15 - 3*a9*b19 - 15*a9*b21,
30*a1*b10 + 10*a1*b12 + 20*a1*b13 + 5*a1*b5 + 5*a1*b6 + 20*a1*b7 + 10*a1*b9 - 
14*a2*b1 - 49*a3*b1 - 42*a4*b1 - 105*a5*b1 - 35*a6*b1 - 140*a7*b1,
20*a1*b10 + 40*a1*b11 + 30*a1*b12 + 10*a1*b13 + 15*a1*b6 + 10*a1*b7 + 40*a1*b8 
+ 35*a1*b9 - 56*a3*b1 - 210*a4*b1 - 182*a5*b1 - 315*a6*b1 - 231*a7*b1,
30*a1*b10 + 10*a1*b11 + 30*a1*b12 + 30*a1*b13 + 5*a1*b6 + 10*a1*b7 + 10*a1*b8 +
 20*a1*b9 - 28*a3*b1 - 84*a4*b1 - 112*a5*b1 - 126*a6*b1 - 210*a7*b1,
20*a1*b14 + 10*a1*b15 + 10*a1*b17 + 5*a1*b21 - 10*a2*b2 + 3*a2*b5 + 3*a2*b7 - 
10*a3*b2 - 10*a5*b2 - 5*a7*b2 - a7*b3 - 140*a8*b1 - 35*a9*b1,
80*a1*b14 + 100*a1*b15 + 80*a1*b17 + 60*a1*b18 + 20*a1*b21 + 30*a1*b22 - 2*a2*
b5 - 6*a3*b5 - 2*a3*b7 - 5*a5*b5 - 2*a7*b5 - 1680*a8*b1 - 700*a9*b1,
180*a1*b15 + 240*a1*b16 + 120*a1*b17 + 270*a1*b18 + 60*a1*b19 + 180*a1*b20 + 90
*a1*b22 - 5*a3*b6 - 10*a4*b6 - 5*a5*b6 - 2*a6*b6 - 5040*a8*b1 - 3780*a9*b1,
10*a1*b17 + 40*a1*b21 + 5*a1*b22 - 8*a2*b10 + 2*a3*b13 + 2*a4*b13 + 2*a5*b13 + 
4*a5*b2 - 4*a7*b10 - 4*a7*b3 - a7*b9 - 56*a8*b1 - 98*a9*b1,
20*a1*b21 + 5*a1*b22 - 20*a2*b13 - 6*a3*b13 - 5*a5*b13 + a6*b13 + 3*a7*b10 - a7
*b11 - 7*a7*b13 + 6*a7*b2 + 3*a7*b3 + a7*b7 - 56*a9*b1,
20*a1*b21 + 15*a1*b22 - 22*a2*b13 - 15*a3*b13 - 15*a5*b13 + 3*a7*b10 - a7*b11 -
 10*a7*b13 + 2*a7*b2 + 3*a7*b3 + 4*a7*b5 + 3*a7*b7 - 112*a9*b1,
720*a1*b23 + 240*a1*b24 + 3*a3*b15 + 3*a3*b17 + 3*a3*b18 + a3*b22 - 48*a8*b3 - 
12*a8*b5 - 24*a8*b7 - 18*a9*b3 - 3*a9*b5 - 4*a9*b6 - 12*a9*b7,
20*a1*b2 + 50*a1*b3 + 60*a1*b4 + 40*a1*b5 + 30*a1*b6 + 10*a1*b7 + 10*a1*b8 + 5*
a1*b9 - 420*a2*b1 - 350*a3*b1 - 210*a4*b1 - 140*a5*b1 - 63*a6*b1 - 21*a7*b1,
5*a1*b10 + 10*a1*b2 + 25*a1*b3 + 20*a1*b4 + 30*a1*b5 + 10*a1*b6 + 20*a1*b7 + 5*
a1*b9 - 210*a2*b1 - 175*a3*b1 - 70*a4*b1 - 105*a5*b1 - 21*a6*b1 - 42*a7*b1,
a1*b11 + 2*a1*b3 + 6*a1*b4 + 4*a1*b5 + 6*a1*b6 + 2*a1*b7 + 4*a1*b8 + 2*a1*b9 - 
28*a2*b1 - 42*a3*b1 - 42*a4*b1 - 28*a5*b1 - 21*a6*b1 - 7*a7*b1,
120*a1*b14 + 30*a1*b15 + 10*a1*b16 + 5*a1*b17 - 54*a2*b2 + 9*a2*b3 + 6*a2*b4 + 
3*a2*b5 - 30*a3*b2 - 10*a4*b2 - 5*a5*b2 - 2*a6*b2 - 420*a8*b1 - 63*a9*b1,
240*a1*b14 + 120*a1*b15 + 20*a1*b16 + 20*a1*b17 + 40*a1*b18 + 5*a1*b20 + 5*a1*
b22 - 6*a2*b4 - 6*a2*b5 - a3*b3 - 3*a3*b4 - 3*a3*b5 - 1680*a8*b1 - 420*a9*b1,
160*a1*b14 + 80*a1*b15 + 40*a1*b17 + 20*a1*b18 + 10*a1*b21 + 5*a1*b22 - 10*a2*
b3 - 4*a2*b7 - 6*a3*b3 + 2*a3*b5 - 5*a5*b3 - 2*a7*b3 - 1120*a8*b1 - 280*a9*b1,
180*a1*b23 + 30*a1*b24 + 6*a2*b14 + 9*a2*b15 + 6*a2*b16 + 3*a2*b17 + 2*a2*b19 -
 9*a3*b14 - 6*a4*b14 - 3*a5*b14 - 4*a6*b14 - 120*a8*b2 - 30*a9*b2 - 3*a9*b5,
360*a1*b23 + 60*a1*b24 + 12*a2*b14 + 9*a2*b15 + 3*a2*b17 + 3*a2*b18 + a2*b22 - 
120*a8*b2 - 12*a8*b3 - 12*a8*b5 - 30*a9*b2 - 2*a9*b3 - a9*b4 - 5*a9*b5,
360*a1*b23 + 120*a1*b24 + 6*a2*b15 + 6*a2*b16 + 6*a2*b18 + 3*a2*b20 + a3*b20 - 
120*a8*b2 - 12*a8*b4 - 4*a8*b6 - 60*a9*b2 - 3*a9*b4 - 2*a9*b6 - 6*a9*b7,
720*a1*b23 + 240*a1*b24 + 3*a3*b15 + 3*a3*b16 + 3*a3*b18 + a3*b20 - 48*a8*b3 - 
12*a8*b4 - 4*a8*b6 - 12*a8*b7 - 18*a9*b3 - 3*a9*b4 - 5*a9*b6 - 9*a9*b7,
360*a1*b23 + 120*a1*b24 + 6*a2*b15 + 6*a2*b17 + 6*a2*b18 + 3*a2*b22 + a3*b22 - 
120*a8*b2 - 12*a8*b5 - 12*a8*b7 - 60*a9*b2 - 3*a9*b5 - a9*b6 - 9*a9*b7,
40*a1*b24 - 2*a2*b21 + 3*a2*b22 - 3*a3*b21 - 3*a5*b21 + 4*a7*b14 + 3*a7*b15 + 3
*a7*b17 + 3*a7*b22 - 40*a8*b13 - a9*b11 - 30*a9*b13 - 20*a9*b2 + a9*b5,
36*a2*b23 + 18*a2*b24 + a3*b24 + a4*b24 + 9*a5*b23 + 8*a5*b24 - 12*a8*b14 - 6*
a8*b17 + 2*a8*b22 - 9*a9*b14 - a9*b15 - a9*b16 - 6*a9*b17 - a9*b18,
12*a2*b23 + 6*a2*b24 + 6*a3*b23 + 2*a3*b24 + 2*a4*b24 + 6*a5*b23 + 4*a5*b24 - 2
*a8*b15 - 2*a8*b17 - 2*a8*b18 - a9*b15 - a9*b16 - a9*b17 - 2*a9*b18,
24*a2*b24 + 4*a3*b24 + 8*a6*b24 + 72*a7*b23 + 48*a7*b24 - 24*a8*b21 - 8*a8*b22 
- a9*b15 + a9*b17 + a9*b18 - 4*a9*b19 - a9*b20 - 12*a9*b21 - 5*a9*b22,
20*a1*b10 + 5*a1*b12 + 5*a1*b13 + 5*a1*b3 + 10*a1*b4 + 20*a1*b5 + 10*a1*b6 + 30
*a1*b7 + 10*a1*b9 - 84*a2*b1 - 126*a3*b1 - 70*a4*b1 - 140*a5*b1 - 35*a6*b1 - 
105*a7*b1,
2*a1*b10 + 6*a1*b11 + 2*a1*b12 + 4*a1*b4 + 3*a1*b5 + 10*a1*b6 + 5*a1*b7 + 12*a1
*b8 + 8*a1*b9 - 14*a2*b1 - 49*a3*b1 - 84*a4*b1 - 63*a5*b1 - 70*a6*b1 - 35*a7*b1
,
30*a1*b15 + 70*a1*b17 + 40*a1*b18 + 60*a1*b21 + 40*a1*b22 - 6*a2*b7 + a3*b3 - 3
*a3*b7 - 3*a5*b5 - 3*a5*b7 - 3*a7*b5 - a7*b6 - 3*a7*b7 - 840*a8*b1 - 630*a9*b1,
5*a1*b17 + 5*a1*b19 + 20*a1*b21 + 3*a2*b10 + 3*a2*b12 + 6*a2*b13 + a5*b12 + 2*
a5*b13 - 5*a5*b2 - a6*b10 - 5*a6*b2 - 4*a7*b10 - 20*a7*b2 - 28*a8*b1 - 49*a9*b1
,
30*a1*b17 + 20*a1*b18 + 50*a1*b21 + 50*a1*b22 - 10*a2*b10 - 10*a3*b10 - 10*a5*
b10 + a5*b3 + 3*a5*b5 + 2*a5*b7 - 6*a7*b10 - 2*a7*b7 - a7*b9 - 280*a8*b1 - 490*
a9*b1,
60*a1*b19 + 40*a1*b20 + 20*a1*b21 + 20*a1*b22 - 2*a2*b11 - 2*a3*b11 - 6*a4*b12 
- 4*a5*b12 + 2*a6*b11 - 12*a6*b12 - 3*a6*b4 + 2*a6*b8 + a6*b9 - 4*a7*b12 - 560*
a9*b1,
10*a1*b19 + 40*a1*b21 + 5*a1*b22 - 8*a2*b12 + 2*a3*b13 - 2*a4*b13 - 5*a5*b13 - 
3*a6*b13 + 4*a6*b2 + 3*a7*b10 - a7*b12 - 14*a7*b13 - 4*a7*b3 + a7*b9 - 112*a9*
b1,
90*a1*b23 + 30*a1*b24 + 3*a2*b15 + 6*a2*b16 + 3*a2*b17 + 3*a2*b19 - 3*a3*b14 + 
a3*b19 - 6*a4*b14 - 3*a5*b14 - 3*a6*b14 - a6*b15 - 60*a8*b2 - 30*a9*b2 - 3*a9*
b7,
2*a1*b10 + a1*b11 + a1*b12 + 3*a1*b3 + 8*a1*b4 + 7*a1*b5 + 8*a1*b6 + 6*a1*b7 + 
4*a1*b8 + 4*a1*b9 - 42*a2*b1 - 63*a3*b1 - 56*a4*b1 - 49*a5*b1 - 28*a6*b1 - 21*
a7*b1,
30*a1*b10 + 10*a1*b11 + 20*a1*b12 + 10*a1*b13 + 10*a1*b4 + 10*a1*b5 + 25*a1*b6 
+ 30*a1*b7 + 20*a1*b8 + 30*a1*b9 - 42*a2*b1 - 147*a3*b1 - 210*a4*b1 - 231*a5*b1
 - 175*a6*b1 - 210*a7*b1,
40*a1*b14 + 50*a1*b15 + 60*a1*b17 + 20*a1*b18 + 40*a1*b21 + 10*a1*b22 - 4*a2*b5
 - 4*a3*b3 + 2*a3*b7 - 6*a5*b3 - a5*b5 - 4*a7*b3 - 2*a7*b4 - 2*a7*b5 - 840*a8*
b1 - 350*a9*b1,
30*a1*b15 + 10*a1*b16 + 60*a1*b17 + 40*a1*b18 + 10*a1*b20 + 60*a1*b21 + 30*a1*
b22 - 6*a2*b7 + a3*b3 - 3*a3*b7 - 3*a5*b4 - a5*b6 - 3*a7*b4 - 2*a7*b6 - 840*a8*
b1 - 630*a9*b1,
10*a1*b15 + 40*a1*b17 + 10*a1*b18 + 60*a1*b21 + 10*a1*b22 - 6*a2*b7 + 3*a3*b10 
+ 2*a3*b13 + 2*a3*b2 - 4*a5*b3 - a5*b7 - 6*a7*b3 - a7*b6 - 3*a7*b7 - 336*a8*b1 
- 252*a9*b1,
20*a1*b17 + 10*a1*b18 + 5*a1*b20 + 60*a1*b21 + 20*a1*b22 - 12*a2*b10 - 4*a3*b10
 + 2*a4*b10 + 2*a4*b13 + 2*a5*b2 + 2*a5*b3 - a5*b9 - 3*a7*b4 - 3*a7*b9 - 168*a8
*b1 - 294*a9*b1,
20*a1*b17 + 10*a1*b18 + 60*a1*b21 + 25*a1*b22 - 12*a2*b10 - 5*a3*b10 - 2*a5*b10
 + 2*a5*b13 + 2*a5*b2 + 2*a5*b3 + a5*b7 - 6*a7*b10 - 3*a7*b5 - 2*a7*b8 - 168*a8
*b1 - 294*a9*b1,
360*a1*b23 + 60*a1*b24 + 12*a2*b14 + 8*a2*b15 + 3*a2*b16 + 3*a2*b18 + a2*b20 + 
2*a3*b14 - 120*a8*b2 - 12*a8*b3 - 10*a8*b4 - 2*a8*b5 - 30*a9*b2 - 2*a9*b3 - 2*
a9*b4 - 4*a9*b5,
30*a1*b23 + 25*a1*b24 + 3*a2*b17 + 3*a2*b19 + 6*a2*b21 - 3*a5*b14 + a5*b19 + 2*
a5*b21 - 3*a6*b14 - a6*b17 - 6*a7*b14 - 2*a7*b17 + 4*a8*b12 - 20*a8*b2 - 5*a9*
b10 - 25*a9*b2,
360*a1*b23 + 300*a1*b24 + a3*b22 + a4*b22 + 3*a5*b15 + 3*a5*b17 + 3*a5*b18 + 2*
a5*b22 - 60*a8*b10 - 12*a8*b3 - 12*a8*b5 - 30*a9*b10 - 12*a9*b3 - 9*a9*b5 - 6*
a9*b8 - 3*a9*b9,
60*a1*b14 + 30*a1*b15 + 20*a1*b16 + 10*a1*b17 + 5*a1*b19 - 30*a2*b2 + 3*a2*b3 +
 6*a2*b4 + 3*a2*b5 + 3*a2*b6 - 30*a3*b2 - 20*a4*b2 - 10*a5*b2 - 5*a6*b2 - a6*b3
 - 420*a8*b1 - 105*a9*b1,
240*a1*b14 + 300*a1*b15 + 180*a1*b16 + 60*a1*b17 + 180*a1*b18 + 20*a1*b19 + 70*
a1*b20 + 20*a1*b22 - 6*a2*b4 - 2*a2*b6 - 11*a3*b4 - 2*a3*b6 - 10*a4*b4 - 5*a5*
b4 - 2*a6*b4 - 5040*a8*b1 - 2100*a9*b1,
240*a1*b14 + 300*a1*b15 + 120*a1*b16 + 120*a1*b17 + 180*a1*b18 + 20*a1*b19 + 40
*a1*b20 + 50*a1*b22 - 6*a2*b5 - 2*a3*b4 - 12*a3*b5 - 2*a3*b6 - 10*a4*b5 - 5*a5*
b5 - 2*a6*b5 - 5040*a8*b1 - 2100*a9*b1,
80*a1*b14 + 100*a1*b15 + 20*a1*b16 + 60*a1*b17 + 60*a1*b18 + 10*a1*b20 + 20*a1*
b21 + 20*a1*b22 - 2*a2*b5 - 2*a2*b7 - 3*a3*b4 - 2*a3*b5 - 2*a3*b7 - 5*a5*b4 - 2
*a7*b4 - 1680*a8*b1 - 700*a9*b1,
90*a1*b15 + 150*a1*b16 + 60*a1*b17 + 120*a1*b18 + 60*a1*b19 + 90*a1*b20 + 30*a1
*b22 - 3*a3*b4 - a3*b6 - 6*a4*b4 - 2*a4*b6 - 3*a5*b4 - a5*b6 - 3*a6*b4 - 2*a6*
b6 - 2520*a8*b1 - 1890*a9*b1,
180*a1*b16 + 90*a1*b17 + 180*a1*b18 + 150*a1*b19 + 300*a1*b20 + 150*a1*b22 - 6*
a3*b8 - 3*a3*b9 - 12*a4*b8 - 6*a4*b9 - 6*a5*b8 - 3*a5*b9 - 2*a6*b6 - 6*a6*b8 - 
3*a6*b9 - 2520*a8*b1 - 4410*a9*b1,
20*a1*b19 + 15*a1*b20 + 60*a1*b21 + 20*a1*b22 - 12*a2*b12 - 4*a3*b12 - 2*a4*b12
 - 4*a5*b12 + 2*a6*b10 - 2*a6*b12 + 2*a6*b13 + 2*a6*b2 + 2*a6*b3 + a6*b9 - 12*
a7*b12 - 3*a7*b4 - 336*a9*b1,
60*a1*b24 + 3*a2*b22 - 3*a3*b21 - a5*b19 + a6*b17 + 2*a6*b21 + 12*a7*b14 + 3*a7
*b15 - 2*a7*b19 + 6*a7*b21 + 3*a7*b22 - 4*a8*b12 - 40*a8*b13 - 5*a9*b12 - 35*a9
*b13 - 30*a9*b2 + a9*b3,
120*a1*b24 - 4*a2*b22 + 4*a3*b21 - a5*b22 + 4*a6*b21 + a6*b22 + 24*a7*b14 + 6*
a7*b15 + 6*a7*b17 + 2*a7*b18 - 2*a7*b20 + 12*a7*b21 + a7*b22 - 120*a8*b13 - 12*
a9*b12 - 60*a9*b13 - 8*a9*b3,
24*a2*b24 + 6*a3*b24 + 12*a6*b23 + 10*a6*b24 + 36*a7*b23 + 42*a7*b24 - 4*a8*b19
 - 6*a8*b20 - 12*a8*b21 - 2*a8*b22 - 3*a9*b15 + a9*b16 + a9*b18 - 5*a9*b19 - 2*
a9*b20 - 9*a9*b21 - 4*a9*b22,
480*a1*b14 + 240*a1*b15 + 80*a1*b16 + 40*a1*b17 + 60*a1*b18 + 10*a1*b19 + 10*a1
*b20 + 5*a1*b22 - 24*a2*b3 - 4*a2*b6 - 16*a3*b3 + 4*a3*b4 + 2*a3*b5 - 10*a4*b3 
- 5*a5*b3 - 2*a6*b3 - 3360*a8*b1 - 840*a9*b1,
90*a1*b15 + 120*a1*b16 + 90*a1*b17 + 120*a1*b18 + 60*a1*b19 + 60*a1*b20 + 60*a1
*b22 - 3*a3*b5 - 3*a3*b7 - 6*a4*b5 - 6*a4*b7 - 3*a5*b5 - 3*a5*b7 - 3*a6*b5 - a6
*b6 - 3*a6*b7 - 2520*a8*b1 - 1890*a9*b1,
20*a1*b16 + 15*a1*b17 + 50*a1*b19 + 25*a1*b21 + 9*a2*b11 + 3*a2*b12 + 6*a2*b8 +
 3*a2*b9 - 20*a4*b2 + 3*a5*b11 + a5*b12 - 15*a5*b2 - 10*a6*b10 - 50*a6*b2 - 5*
a7*b10 - 25*a7*b2 - 140*a8*b1 - 245*a9*b1,
60*a1*b23 + 50*a1*b24 + 6*a2*b16 + 3*a2*b17 + 9*a2*b19 + 3*a2*b21 - 6*a4*b14 - 
3*a5*b14 + 3*a5*b19 + a5*b21 - 9*a6*b14 - 3*a6*b17 - 3*a7*b14 - a7*b17 + 4*a8*
b11 - 40*a8*b2 - 10*a9*b10 - 50*a9*b2,
360*a1*b24 - a3*b20 + 2*a6*b16 + 2*a6*b17 + 4*a6*b18 + 3*a6*b20 + 2*a6*b22 + 6*
a7*b15 + 6*a7*b16 + 6*a7*b18 + 3*a7*b20 - 48*a8*b12 - 120*a8*b13 - 6*a9*b11 - 
48*a9*b12 - 60*a9*b13 - 12*a9*b4 - 6*a9*b5,
60*a1*b24 + 3*a2*b22 - 4*a3*b21 - 3*a5*b21 + a6*b21 + 12*a7*b14 + 4*a7*b15 + 3*
a7*b17 - a7*b19 + 6*a7*b21 + 3*a7*b22 - 60*a8*b13 - a9*b11 - a9*b12 - 45*a9*b13
 - 30*a9*b2 + a9*b3 + a9*b7,
36*a2*b23 + 18*a2*b24 + 3*a3*b23 + a3*b24 + 6*a4*b23 + 2*a4*b24 + 3*a5*b23 + 7*
a5*b24 - 12*a8*b14 - 2*a8*b15 - 4*a8*b16 - 2*a8*b17 + 2*a8*b20 - 9*a9*b14 - a9*
b15 - 3*a9*b16 - 4*a9*b17 - a9*b18,
48*a2*b24 + 2*a3*b24 - 2*a4*b24 - a5*b24 + 18*a6*b23 - a6*b24 + 18*a7*b23 + 57*
a7*b24 - 12*a8*b19 - 12*a8*b21 - 24*a9*b14 - 2*a9*b15 + 2*a9*b16 + a9*b17 - a9*
b19 + 2*a9*b20 - 33*a9*b21 - 2*a9*b22,
10*a1*b15 + 30*a1*b16 + 20*a1*b17 + 30*a1*b19 + 10*a1*b21 + 3*a2*b11 + 3*a2*b6 
+ 6*a2*b8 + 3*a2*b9 + a3*b11 - 10*a3*b2 - 30*a4*b2 - 20*a5*b2 - 30*a6*b2 - 3*a6
*b7 - 10*a7*b2 - a7*b7 - 280*a8*b1 - 210*a9*b1,
60*a1*b19 + 30*a1*b20 + 20*a1*b21 + 30*a1*b22 - 2*a2*b11 - 2*a3*b11 - 10*a3*b13
 - 30*a4*b13 - 20*a5*b13 - 2*a6*b11 - 30*a6*b13 - 3*a6*b5 + 2*a7*b11 - 10*a7*
b13 + 3*a7*b6 + a7*b7 + 6*a7*b8 + 3*a7*b9 - 560*a9*b1,
80*a1*b19 + 55*a1*b20 + 60*a1*b21 + 35*a1*b22 - 6*a2*b11 - 3*a3*b11 - a3*b12 - 
8*a4*b12 - 7*a5*b12 + a6*b10 + 2*a6*b11 - 14*a6*b12 + a6*b3 - 3*a6*b4 + 2*a6*b8
 + 2*a6*b9 - 12*a7*b12 - 3*a7*b4 - 840*a9*b1,
70*a1*b19 + 140*a1*b20 + 30*a1*b21 + 100*a1*b22 - 6*a2*b12 - 4*a3*b11 - 12*a3*
b12 - 8*a4*b11 - 12*a4*b12 - 7*a5*b11 - 6*a5*b12 - 5*a6*b11 - 4*a6*b12 + 2*a6*
b4 + a6*b5 + 3*a6*b6 + a6*b7 - 3*a7*b11 - 1680*a9*b1,
10*a1*b19 + 20*a1*b20 + 30*a1*b21 + 40*a1*b22 - 30*a2*b13 - a3*b11 - 30*a3*b13 
- 20*a4*b13 - 3*a5*b11 - 10*a5*b13 - a6*b12 - 5*a6*b13 + a6*b7 - 3*a7*b11 + 3*
a7*b3 + 6*a7*b4 + 3*a7*b5 + 3*a7*b6 - 420*a9*b1,
20*a1*b19 + 40*a1*b20 + 20*a1*b21 + 40*a1*b22 - 4*a2*b12 - 8*a3*b12 - a4*b11 - 
6*a4*b12 - a5*b11 - 6*a5*b12 - a6*b11 - 2*a6*b12 + a6*b4 + a6*b5 + a6*b6 + a6*
b7 - a7*b11 - 2*a7*b12 - 560*a9*b1,
10*a1*b20 + 60*a1*b21 + 35*a1*b22 - 60*a2*b13 - a3*b12 - 30*a3*b13 - 10*a4*b13 
- a5*b11 - 4*a5*b12 - 5*a5*b13 + 3*a6*b10 + a6*b7 - 3*a7*b11 - 6*a7*b12 + 6*a7*
b2 + 9*a7*b3 + 6*a7*b4 + 3*a7*b5 - 336*a9*b1,
120*a1*b23 + 40*a1*b24 + 3*a2*b15 + 6*a2*b16 + 6*a2*b17 + 3*a2*b19 + 3*a2*b21 -
 3*a3*b14 + a3*b19 + a3*b21 - 6*a4*b14 - 6*a5*b14 - 3*a6*b14 - a6*b15 - 3*a7*
b14 - a7*b15 - 80*a8*b2 - 40*a9*b2 - 4*a9*b7,
360*a1*b23 + 300*a1*b24 + a3*b16 + a3*b18 + a3*b20 + 2*a4*b16 + 2*a4*b18 + 2*a4
*b20 + a5*b16 + a5*b18 + a5*b20 - 12*a8*b10 - 12*a8*b3 - 12*a8*b4 - 12*a8*b9 - 
12*a9*b10 - 12*a9*b3 - 9*a9*b4 - 12*a9*b9,
480*a1*b24 - 4*a2*b22 - a3*b22 - 3*a5*b22 + 4*a6*b21 + 4*a6*b22 + 24*a7*b14 + 
26*a7*b15 + 26*a7*b17 + 18*a7*b18 + 12*a7*b21 + 10*a7*b22 - 480*a8*b13 - 14*a9*
b11 - 20*a9*b12 - 240*a9*b13 - 20*a9*b3 - 6*a9*b5 - 4*a9*b7,
120*a1*b15 + 80*a1*b16 + 160*a1*b17 + 180*a1*b18 + 20*a1*b19 + 60*a1*b20 + 60*
a1*b21 + 120*a1*b22 - 6*a2*b7 + 2*a3*b4 + a3*b5 - a3*b6 - 11*a3*b7 - 10*a4*b7 -
 5*a5*b6 - 5*a5*b7 - 2*a6*b7 - 2*a7*b6 - 3360*a8*b1 - 2520*a9*b1,
10*a1*b16 + 10*a1*b17 + 25*a1*b19 + 30*a1*b21 + 3*a2*b10 + 3*a2*b11 + 6*a2*b12 
+ 3*a2*b13 + 3*a2*b9 - 10*a4*b2 + a5*b11 + 2*a5*b12 + a5*b13 - 10*a5*b2 - 5*a6*
b10 - 25*a6*b2 - 6*a7*b10 - 30*a7*b2 - 84*a8*b1 - 147*a9*b1,
50*a1*b16 + 60*a1*b17 + 50*a1*b18 + 60*a1*b19 + 65*a1*b20 + 120*a1*b21 + 60*a1*
b22 - 6*a2*b9 - 3*a3*b9 + 2*a4*b10 + 2*a4*b12 + 2*a4*b3 - 3*a5*b4 - 3*a5*b9 - 3
*a6*b4 - 3*a6*b9 - 6*a7*b4 - 6*a7*b9 - 840*a8*b1 - 1470*a9*b1,
50*a1*b19 + 10*a1*b20 + 60*a1*b21 + 10*a1*b22 - 6*a2*b11 + 2*a3*b12 - 10*a4*b13
 - 11*a5*b13 + a6*b11 - 3*a6*b12 - 24*a6*b13 + 2*a6*b2 - 4*a6*b3 + 3*a7*b10 + 3
*a7*b11 - 27*a7*b13 - 6*a7*b3 + 2*a7*b8 + 3*a7*b9 - 336*a9*b1,
720*a1*b23 + 240*a1*b24 + 12*a2*b15 + 6*a2*b16 + 6*a2*b17 + 12*a2*b18 + 3*a2*
b20 + 3*a2*b22 + a3*b20 + a3*b22 - 240*a8*b2 - 12*a8*b4 - 12*a8*b5 - 4*a8*b6 - 
12*a8*b7 - 120*a9*b2 - 3*a9*b4 - 3*a9*b5 - 3*a9*b6 - 15*a9*b7,
480*a1*b23 + 160*a1*b24 + 4*a2*b15 + 12*a2*b17 + 6*a2*b18 + 6*a2*b21 + 3*a2*b22
 + 4*a3*b14 + 3*a3*b17 + 4*a3*b21 + a3*b22 - 3*a5*b15 - 4*a7*b15 - 160*a8*b2 - 
16*a8*b3 - 24*a8*b7 - 80*a9*b2 - 6*a9*b3 - a9*b6 - 13*a9*b7,
120*a1*b23 + 100*a1*b24 + 2*a2*b17 + 12*a2*b21 + 3*a2*b22 + 2*a3*b21 + 2*a4*b21
 + 8*a5*b14 + 6*a5*b21 + a5*b22 - 2*a7*b15 - 2*a7*b16 - 2*a7*b17 - 2*a7*b18 - 
20*a8*b10 - 40*a8*b2 - 16*a9*b10 - 50*a9*b2 - 4*a9*b3 - a9*b9,
240*a1*b23 + 200*a1*b24 + 4*a2*b17 + 6*a2*b18 + 6*a2*b21 + 9*a2*b22 - 3*a3*b17 
+ 4*a5*b14 + 3*a5*b15 + 4*a5*b21 + 3*a5*b22 - 4*a7*b17 - 40*a8*b10 - 80*a8*b2 -
 30*a9*b10 - 100*a9*b2 - 3*a9*b5 - 2*a9*b7 - 2*a9*b8 - a9*b9,
360*a1*b24 + 4*a3*b19 + 2*a3*b20 - 2*a4*b22 - a5*b22 + 2*a6*b15 + 4*a6*b19 - a6
*b22 + 12*a7*b16 + 6*a7*b17 + 6*a7*b18 + 12*a7*b19 + 6*a7*b20 + 3*a7*b22 - 24*
a8*b11 - 120*a8*b13 - 6*a9*b11 - 30*a9*b12 - 150*a9*b13 - 30*a9*b3,
360*a1*b24 - a3*b20 - a3*b22 + 2*a6*b17 + 2*a6*b18 + a6*b20 + 3*a6*b22 + 12*a7*
b15 + 6*a7*b16 + 6*a7*b17 + 12*a7*b18 + 3*a7*b20 + 3*a7*b22 - 24*a8*b12 - 240*
a8*b13 - 12*a9*b11 - 24*a9*b12 - 120*a9*b13 - 6*a9*b4 - 12*a9*b5,
80*a1*b14 + 40*a1*b15 + 20*a1*b16 + 20*a1*b17 + 5*a1*b19 + 5*a1*b21 - 40*a2*b2 
+ 3*a2*b3 + 6*a2*b4 + 6*a2*b5 + 3*a2*b6 + 3*a2*b7 - 40*a3*b2 - 20*a4*b2 - 20*a5
*b2 - 5*a6*b2 - a6*b3 - 5*a7*b2 - a7*b3 - 560*a8*b1 - 140*a9*b1,
120*a1*b14 + 150*a1*b15 + 120*a1*b16 + 60*a1*b17 + 60*a1*b18 + 40*a1*b19 + 20*
a1*b20 + 10*a1*b22 - 6*a2*b3 - 12*a3*b3 + 2*a3*b4 + 2*a3*b6 - 12*a4*b3 - 2*a4*
b5 - 6*a5*b3 - a5*b5 - 4*a6*b3 - 2*a6*b4 - 2*a6*b5 - 2520*a8*b1 - 1050*a9*b1,
5*a1*b15 + 10*a1*b16 + 20*a1*b17 + 10*a1*b19 + 30*a1*b21 + 6*a2*b10 + 3*a2*b12 
+ 3*a2*b13 + 3*a2*b7 + 3*a2*b9 + a3*b12 + a3*b13 - 5*a3*b2 - 10*a4*b2 - 20*a5*
b2 - 10*a6*b2 - a6*b7 - 30*a7*b2 - 3*a7*b7 - 168*a8*b1 - 126*a9*b1,
120*a1*b15 + 160*a1*b16 + 120*a1*b17 + 160*a1*b18 + 60*a1*b19 + 100*a1*b20 + 60
*a1*b21 + 60*a1*b22 - 2*a2*b6 - 3*a3*b4 - 2*a3*b6 - 6*a4*b4 - 2*a4*b6 - 6*a5*b4
 - 2*a5*b6 - 3*a6*b4 - 2*a6*b6 - 3*a7*b4 - 2*a7*b6 - 3360*a8*b1 - 2520*a9*b1,
100*a1*b19 + 20*a1*b20 + 50*a1*b21 + 15*a1*b22 - 4*a2*b11 - 2*a2*b12 + 2*a3*b11
 - 20*a4*b13 - 15*a5*b13 + 3*a6*b11 - 9*a6*b12 - 50*a6*b13 - 10*a6*b3 + a7*b10 
+ 9*a7*b11 - 2*a7*b12 - 25*a7*b13 - 4*a7*b3 + 6*a7*b8 + 4*a7*b9 - 560*a9*b1,
240*a1*b23 + 200*a1*b24 - 2*a2*b18 + 2*a3*b17 + 2*a3*b21 + a3*b22 + 2*a4*b21 + 
a4*b22 + 4*a5*b14 + 2*a5*b15 + 2*a5*b17 + 2*a5*b21 + a5*b22 - 2*a7*b18 - 40*a8*
b10 - 16*a8*b3 - 4*a8*b7 - 20*a9*b10 - 16*a9*b3 - 2*a9*b7 - 5*a9*b9,
180*a1*b24 + 6*a2*b19 + 9*a2*b20 + 3*a2*b22 - a3*b19 - 2*a4*b19 - a5*b19 + a6*
b15 + 2*a6*b16 + a6*b17 - a6*b20 + 6*a7*b19 + 9*a7*b20 + 3*a7*b22 - 12*a8*b11 -
 12*a8*b12 - 3*a9*b11 - 12*a9*b12 - 90*a9*b13 - 90*a9*b2 - 3*a9*b4,
360*a1*b24 + 6*a2*b19 + 18*a2*b20 + 9*a2*b22 - 3*a3*b19 - 6*a4*b19 - 3*a5*b19 +
 3*a6*b15 + 6*a6*b16 + 3*a6*b17 - 2*a6*b19 + 6*a7*b19 + 18*a7*b20 + 9*a7*b22 - 
12*a8*b11 - 48*a8*b12 - 9*a9*b11 - 18*a9*b12 - 180*a9*b13 - 180*a9*b2 - 2*a9*b6
,
20*a1*b14 + 25*a1*b15 + 20*a1*b16 + 30*a1*b17 + 10*a1*b19 + 20*a1*b21 + 3*a2*
b10 + 2*a2*b12 - 10*a2*b2 + 3*a2*b5 + 3*a2*b6 + 6*a2*b7 + 3*a2*b9 - 25*a3*b2 - 
20*a4*b2 - 30*a5*b2 - 10*a6*b2 - a6*b5 - 20*a7*b2 - 2*a7*b5 - 420*a8*b1 - 175*
a9*b1,
140*a1*b16 + 80*a1*b17 + 100*a1*b18 + 180*a1*b19 + 170*a1*b20 + 60*a1*b21 + 80*
a1*b22 - 4*a2*b8 - 4*a3*b8 - a3*b9 + 2*a4*b11 - 6*a4*b4 + 4*a4*b8 - 4*a4*b9 - 3
*a5*b4 - 4*a5*b9 - 9*a6*b4 - 9*a6*b9 - 3*a7*b4 - 3*a7*b9 - 1680*a8*b1 - 2940*a9
*b1,
200*a1*b19 + 280*a1*b20 + 60*a1*b21 + 170*a1*b22 - 6*a2*b11 - 12*a3*b11 - 10*a3
*b12 - 16*a4*b11 - 24*a4*b12 - 9*a5*b11 - 16*a5*b12 - 9*a6*b11 - 18*a6*b12 + 2*
a6*b4 + a6*b5 + a6*b6 + a6*b7 + 6*a6*b8 + 3*a6*b9 - 3*a7*b11 - 6*a7*b12 - 3360*
a9*b1,
40*a1*b14 + 50*a1*b15 + 60*a1*b16 + 40*a1*b17 + 30*a1*b19 + 10*a1*b21 + 2*a2*
b11 - 20*a2*b2 + 6*a2*b4 + 3*a2*b5 + 9*a2*b6 + 3*a2*b7 + 6*a2*b8 + 3*a2*b9 - 50
*a3*b2 - 60*a4*b2 - 40*a5*b2 - 30*a6*b2 - 3*a6*b5 - 10*a7*b2 - a7*b5 - 840*a8*
b1 - 350*a9*b1,
15*a1*b15 + 40*a1*b16 + 35*a1*b17 + 40*a1*b19 + 30*a1*b21 + 3*a2*b10 + 3*a2*b11
 + 3*a2*b12 + 3*a2*b6 + 3*a2*b7 + 6*a2*b8 + 6*a2*b9 + a3*b11 + a3*b12 - 15*a3*
b2 - 40*a4*b2 - 35*a5*b2 - 40*a6*b2 - 4*a6*b7 - 30*a7*b2 - 3*a7*b7 - 420*a8*b1 
- 315*a9*b1,
40*a1*b16 + 50*a1*b17 + 60*a1*b18 + 40*a1*b19 + 60*a1*b20 + 30*a1*b21 + 90*a1*
b22 - 6*a2*b10 - 12*a3*b10 - 2*a3*b8 - 12*a4*b10 - 2*a4*b7 - 6*a5*b10 + 2*a5*b4
 + a5*b5 + 2*a5*b6 - 4*a5*b8 - 4*a6*b10 - 2*a6*b7 - a6*b9 - 2*a7*b8 - 840*a8*b1
 - 1470*a9*b1,
20*a1*b19 + 10*a1*b20 + 60*a1*b21 + 25*a1*b22 - 12*a2*b12 - 4*a3*b12 - 6*a3*b13
 - 10*a4*b13 - 20*a5*b13 - a6*b11 + a6*b12 - 9*a6*b13 + 2*a6*b2 + 2*a6*b3 + 6*
a7*b10 - 3*a7*b11 + 3*a7*b12 - 27*a7*b13 - 3*a7*b5 + a7*b6 + 3*a7*b7 + 3*a7*b9 
- 336*a9*b1,
70*a1*b19 + 110*a1*b20 + 120*a1*b21 + 115*a1*b22 - 24*a2*b12 - 23*a3*b12 - 2*a4
*b11 - 18*a4*b12 - 3*a5*b11 - 17*a5*b12 + 3*a6*b10 - 3*a6*b11 - 6*a6*b12 + 3*a6
*b3 + 4*a6*b4 + 2*a6*b5 + a6*b6 + 2*a6*b7 + 3*a6*b9 - 6*a7*b11 - 12*a7*b12 - 2*
a7*b6 - 1680*a9*b1,
120*a1*b15 + 120*a1*b16 + 160*a1*b17 + 160*a1*b18 + 60*a1*b19 + 60*a1*b20 + 60*
a1*b21 + 100*a1*b22 - 2*a2*b6 - 3*a3*b5 - a3*b6 - 3*a3*b7 - 6*a4*b5 - 6*a4*b7 -
 6*a5*b5 - 6*a5*b7 - 3*a6*b5 - a6*b6 - 3*a6*b7 - 3*a7*b5 - a7*b6 - 3*a7*b7 - 
3360*a8*b1 - 2520*a9*b1,
20*a1*b16 + 70*a1*b17 + 60*a1*b18 + 10*a1*b19 + 40*a1*b20 + 120*a1*b21 + 110*a1
*b22 - 24*a2*b10 - 18*a3*b10 - a3*b9 - 8*a4*b10 + 2*a4*b7 - 4*a5*b10 + 3*a5*b3 
+ 4*a5*b4 + 2*a5*b5 - 2*a5*b8 - 3*a5*b9 - 2*a6*b10 - 2*a7*b6 - 4*a7*b8 - 3*a7*
b9 - 840*a8*b1 - 1470*a9*b1,
80*a1*b19 + 40*a1*b20 + 60*a1*b21 + 50*a1*b22 - 6*a2*b11 - 3*a3*b11 - a3*b12 - 
15*a3*b13 - 40*a4*b13 - 35*a5*b13 - 3*a6*b11 + a6*b12 - 40*a6*b13 + a6*b3 - 3*
a6*b5 + 3*a7*b10 + 3*a7*b12 - 30*a7*b13 - 3*a7*b5 + 4*a7*b6 + 3*a7*b7 + 6*a7*b8
 + 6*a7*b9 - 840*a9*b1,
60*a1*b19 + 60*a1*b20 + 40*a1*b21 + 90*a1*b22 - 2*a2*b11 - 20*a2*b13 - 4*a3*b11
 - 50*a3*b13 - 60*a4*b13 - 5*a5*b11 - 40*a5*b13 - 3*a6*b11 - 30*a6*b13 + a6*b5 
- 2*a6*b7 - a7*b11 - 10*a7*b13 + 6*a7*b4 + 4*a7*b5 + 9*a7*b6 + 3*a7*b7 + 6*a7*
b8 + 3*a7*b9 - 1120*a9*b1,
20*a1*b19 + 20*a1*b20 + 50*a1*b21 + 55*a1*b22 - 8*a2*b12 - 10*a2*b13 - 6*a3*b12
 - 25*a3*b13 - 20*a4*b13 - 5*a5*b12 - 30*a5*b13 - a6*b11 - 10*a6*b13 + a6*b3 + 
2*a6*b5 + 3*a7*b10 - 2*a7*b11 - 20*a7*b13 + 2*a7*b4 + 3*a7*b5 + 3*a7*b6 + 4*a7*
b7 + 3*a7*b9 - 560*a9*b1,
180*a1*b24 + 6*a2*b19 + 6*a2*b20 + 6*a2*b22 - a3*b19 - 3*a3*b21 - 6*a4*b21 - 3*
a5*b21 + a6*b15 - 3*a6*b21 - a6*b22 + 3*a7*b15 + 6*a7*b16 + 3*a7*b17 + 9*a7*b19
 + 6*a7*b20 + 6*a7*b22 - 12*a8*b11 - 60*a8*b13 - 6*a9*b11 - 120*a9*b13 - 90*a9*
b2 - 3*a9*b5 + a9*b6,
10*a1*b19 + 20*a1*b20 + 50*a1*b21 + 60*a1*b22 - 2*a2*b12 - 40*a2*b13 - 4*a3*b12
 - 40*a3*b13 - 20*a4*b13 - a5*b11 - 6*a5*b12 - 20*a5*b13 - a6*b12 - 5*a6*b13 + 
a6*b5 + 2*a6*b7 - 2*a7*b11 - 5*a7*b12 - 5*a7*b13 + 4*a7*b3 + 6*a7*b4 + 6*a7*b5 
+ 3*a7*b6 + 3*a7*b7 - 560*a9*b1,
1440*a1*b23 + 480*a1*b24 + 24*a2*b15 + 24*a2*b16 + 12*a2*b17 + 18*a2*b18 + 6*a2
*b19 + 6*a2*b20 + 3*a2*b22 + 6*a3*b16 + 3*a3*b17 + 4*a3*b19 + 2*a3*b20 + a3*b22
 - 6*a4*b15 - 3*a5*b15 - 4*a6*b15 - 480*a8*b2 - 48*a8*b3 - 20*a8*b6 - 12*a8*b7 
- 240*a9*b2 - 18*a9*b3 - 5*a9*b6 - 33*a9*b7,
120*a1*b24 + 2*a2*b19 + 12*a2*b21 + 3*a2*b22 + 2*a3*b21 - 2*a4*b21 - 3*a5*b21 +
 8*a6*b14 - a6*b21 - a6*b22 - 2*a7*b15 + 2*a7*b16 + 3*a7*b17 + 7*a7*b19 + 2*a7*
b20 + 12*a7*b21 + a7*b22 - 20*a8*b12 - 20*a8*b13 + a9*b10 - 3*a9*b12 - 85*a9*
b13 - 60*a9*b2 - 4*a9*b3 + a9*b9,
240*a1*b24 + 4*a2*b19 + 9*a2*b20 + 6*a2*b21 + 6*a2*b22 - 2*a3*b19 - 2*a4*b19 - 
2*a5*b19 + 4*a6*b14 + 2*a6*b15 + 2*a6*b16 + 2*a6*b17 - a6*b20 + 2*a6*b21 + 4*a7
*b19 + 9*a7*b20 + 6*a7*b21 + 6*a7*b22 - 4*a8*b11 - 40*a8*b12 - 2*a9*b11 - 20*a9
*b12 - 120*a9*b13 - 120*a9*b2 - 3*a9*b4,
240*a1*b24 - 2*a2*b20 + 2*a3*b19 + 2*a3*b21 + a3*b22 - a4*b22 - a5*b22 + 4*a6*
b14 + 2*a6*b15 + 2*a6*b19 + 2*a6*b21 + 6*a7*b16 + 6*a7*b17 + 4*a7*b18 + 6*a7*
b19 + 2*a7*b20 + 6*a7*b21 + 2*a7*b22 - 4*a8*b11 - 24*a8*b12 - 80*a8*b13 - 2*a9*
b11 - 24*a9*b12 - 100*a9*b13 - 20*a9*b3,
120*a1*b15 + 240*a1*b16 + 160*a1*b17 + 100*a1*b18 + 180*a1*b19 + 60*a1*b20 + 60
*a1*b21 + 40*a1*b22 - 2*a2*b6 + 2*a3*b11 - 10*a3*b3 + 2*a3*b6 + 6*a3*b8 + 3*a3*
b9 - 24*a4*b3 - 6*a4*b7 - 16*a5*b3 - 4*a5*b7 - 18*a6*b3 - 3*a6*b6 - 9*a6*b7 - 6
*a7*b3 - a7*b6 - 3*a7*b7 - 3360*a8*b1 - 2520*a9*b1,
60*a1*b15 + 80*a1*b16 + 120*a1*b17 + 50*a1*b18 + 60*a1*b19 + 20*a1*b20 + 120*a1
*b21 + 30*a1*b22 - 4*a2*b6 + 3*a3*b10 + 2*a3*b12 - 4*a3*b3 + 2*a3*b7 + 3*a3*b9 
- 8*a4*b3 - 2*a4*b7 - 12*a5*b3 - 3*a5*b7 - 6*a6*b3 - a6*b6 - 3*a6*b7 - 12*a7*b3
 - 2*a7*b6 - 6*a7*b7 - 1680*a8*b1 - 1260*a9*b1,
60*a1*b16 + 40*a1*b17 + 20*a1*b18 + 120*a1*b19 + 30*a1*b20 + 40*a1*b21 + 20*a1*
b22 - 2*a2*b9 + 2*a3*b11 + 2*a3*b8 - 6*a4*b10 + 2*a4*b11 - 6*a4*b3 - 4*a5*b10 +
 2*a5*b11 - 4*a5*b3 + 2*a5*b8 + a5*b9 - 12*a6*b10 - 12*a6*b3 - 3*a6*b9 - 4*a7*
b10 - 4*a7*b3 - a7*b9 - 560*a8*b1 - 980*a9*b1,
40*a1*b16 + 70*a1*b17 + 50*a1*b18 + 60*a1*b19 + 40*a1*b20 + 120*a1*b21 + 85*a1*
b22 - 6*a2*b9 - 5*a3*b10 - 3*a3*b9 - 8*a4*b10 + 2*a4*b3 - 10*a5*b10 + 2*a5*b12 
- 3*a5*b5 + a5*b6 + 2*a5*b7 + 2*a5*b9 - 6*a6*b10 - 3*a6*b5 - 2*a6*b8 - 12*a7*
b10 - 6*a7*b5 - 4*a7*b8 - 840*a8*b1 - 1470*a9*b1,
200*a1*b16 + 160*a1*b17 + 240*a1*b18 + 160*a1*b19 + 340*a1*b20 + 120*a1*b21 + 
260*a1*b22 - 6*a2*b9 - 13*a3*b9 + 4*a4*b4 + 2*a4*b5 + 2*a4*b6 + 2*a4*b7 - 4*a4*
b8 - 14*a4*b9 - 2*a5*b6 - 4*a5*b8 - 10*a5*b9 - 2*a6*b6 - 4*a6*b8 - 5*a6*b9 - 2*
a7*b6 - 4*a7*b8 - 3*a7*b9 - 3360*a8*b1 - 5880*a9*b1,
40*a1*b16 + 80*a1*b17 + 80*a1*b18 + 40*a1*b19 + 60*a1*b20 + 80*a1*b21 + 140*a1*
b22 - 8*a2*b10 - 2*a2*b9 - 16*a3*b10 - 3*a3*b9 - 12*a4*b10 + 2*a4*b5 - 12*a5*
b10 + 2*a5*b4 + 2*a5*b5 + 2*a5*b6 - 4*a5*b9 - 4*a6*b10 - 2*a6*b7 - a6*b9 - 4*a7
*b10 - 2*a7*b7 - 3*a7*b9 - 1120*a8*b1 - 1960*a9*b1,
240*a1*b23 + 200*a1*b24 + 4*a2*b17 + 6*a2*b18 + 3*a2*b20 + 6*a2*b21 + 6*a2*b22 
- 2*a3*b17 + 2*a4*b17 + 2*a4*b21 + 4*a5*b14 + 2*a5*b15 - 2*a5*b16 + a5*b20 + 2*
a5*b21 + 2*a5*b22 - 4*a7*b16 - 24*a8*b10 - 80*a8*b2 - 4*a8*b7 - 4*a8*b9 - 24*a9
*b10 - 100*a9*b2 - 3*a9*b4 - 2*a9*b7 - 4*a9*b9,
480*a1*b24 - 2*a2*b20 - 2*a2*b22 + 2*a3*b21 - 3*a5*b20 + 4*a6*b17 + 2*a6*b18 + 
a6*b20 + 6*a6*b21 + 4*a6*b22 + 24*a7*b14 + 18*a7*b15 + 8*a7*b16 + 6*a7*b17 + 12
*a7*b18 + a7*b20 + 6*a7*b21 + 6*a7*b22 - 32*a8*b12 - 320*a8*b13 - 6*a9*b11 - 52
*a9*b12 - 160*a9*b13 - 20*a9*b3 - 6*a9*b4 - 6*a9*b7,
80*a1*b14 + 100*a1*b15 + 60*a1*b16 + 60*a1*b17 + 40*a1*b18 + 20*a1*b19 + 10*a1*
b20 + 20*a1*b21 + 10*a1*b22 - 4*a2*b3 - 2*a2*b4 - 8*a3*b3 + a3*b5 + a3*b6 + a3*
b7 - 6*a4*b3 - a4*b5 - 6*a5*b3 - a5*b5 - 2*a6*b3 - a6*b4 - a6*b5 - 2*a7*b3 - a7
*b4 - a7*b5 - 1680*a8*b1 - 700*a9*b1,
720*a1*b23 + 600*a1*b24 + a3*b17 + a3*b18 + a3*b20 + a3*b22 + 2*a4*b17 + 2*a4*
b18 + a4*b20 + 2*a4*b22 + 3*a5*b15 + 3*a5*b16 + a5*b17 + 4*a5*b18 + 2*a5*b20 + 
a5*b22 - 72*a8*b10 - 24*a8*b3 - 12*a8*b4 - 12*a8*b5 - 12*a8*b9 - 42*a9*b10 - 24
*a9*b3 - 9*a9*b4 - 9*a9*b5 - 6*a9*b8 - 15*a9*b9,
240*a1*b24 + 16*a2*b19 + 6*a2*b20 + 6*a2*b21 + 3*a2*b22 + 2*a3*b19 - 6*a4*b21 -
 4*a5*b21 + 4*a6*b14 - 2*a6*b15 - 8*a6*b21 - 3*a6*b22 + 6*a7*b16 + 4*a7*b17 + 
26*a7*b19 + 6*a7*b20 + 6*a7*b21 + 3*a7*b22 - 20*a8*b11 - 40*a8*b13 + 2*a9*b11 -
 10*a9*b12 - 170*a9*b13 - 120*a9*b2 - 10*a9*b3 + 2*a9*b8 + a9*b9,
1440*a1*b24 + 2*a3*b20 + a3*b22 - 6*a4*b22 - 3*a5*b22 + 6*a6*b15 + 6*a6*b17 + 6
*a6*b18 + 4*a6*b19 + 6*a6*b20 + 4*a6*b22 + 24*a7*b15 + 36*a7*b16 + 24*a7*b17 + 
36*a7*b18 + 12*a7*b19 + 18*a7*b20 + 18*a7*b22 - 24*a8*b11 - 96*a8*b12 - 720*a8*
b13 - 42*a9*b11 - 96*a9*b12 - 540*a9*b13 - 60*a9*b3 - 24*a9*b5 - 4*a9*b6,
120*a1*b16 + 100*a1*b17 + 100*a1*b18 + 180*a1*b19 + 120*a1*b20 + 60*a1*b21 + 
130*a1*b22 - 4*a2*b8 - 10*a3*b10 - 4*a3*b8 - a3*b9 - 24*a4*b10 - 6*a4*b5 - 16*
a5*b10 + 2*a5*b11 - 3*a5*b5 + 3*a5*b6 + a5*b7 + 4*a5*b8 + 2*a5*b9 - 18*a6*b10 -
 9*a6*b5 - 6*a6*b8 - 6*a7*b10 - 3*a7*b5 - 2*a7*b8 - 1680*a8*b1 - 2940*a9*b1,
20*a1*b16 + 40*a1*b17 + 10*a1*b18 + 40*a1*b19 + 10*a1*b20 + 120*a1*b21 + 20*a1*
b22 - 6*a2*b9 + 2*a3*b10 + 2*a3*b12 + 2*a3*b13 - 2*a4*b10 + 2*a4*b12 + 2*a4*b13
 + 4*a4*b2 - 2*a5*b10 + 2*a5*b12 + 2*a5*b13 - 4*a5*b3 + a5*b9 - 4*a6*b10 - 4*a6
*b3 - a6*b9 - 12*a7*b10 - 12*a7*b3 - 3*a7*b9 - 336*a8*b1 - 588*a9*b1,
720*a1*b23 + 600*a1*b24 + 18*a2*b16 + 6*a2*b17 + 18*a2*b18 + 6*a2*b19 + 21*a2*
b20 + 6*a2*b22 - 2*a3*b16 + 2*a4*b15 + 2*a4*b17 + 2*a4*b19 - 2*a5*b16 + 2*a5*
b19 + 7*a5*b20 + 2*a5*b22 - 4*a6*b16 - 240*a8*b2 - 12*a8*b4 - 4*a8*b6 - 8*a8*b8
 - 24*a8*b9 - 60*a9*b10 - 300*a9*b2 - 9*a9*b4 - 2*a9*b6 - 4*a9*b8 - 12*a9*b9,
1440*a1*b24 + 2*a3*b19 + 4*a3*b20 + 2*a3*b22 - 6*a4*b20 - 3*a5*b20 + 6*a6*b15 +
 14*a6*b16 + 4*a6*b17 + 12*a6*b18 + 6*a6*b19 + 9*a6*b20 + 4*a6*b22 + 18*a7*b16 
+ 6*a7*b17 + 18*a7*b18 + 6*a7*b19 + 21*a7*b20 + 6*a7*b22 - 24*a8*b11 - 192*a8*
b12 - 240*a8*b13 - 18*a9*b11 - 192*a9*b12 - 300*a9*b13 - 60*a9*b3 - 24*a9*b4 - 
6*a9*b6,
240*a1*b24 + 6*a2*b20 + 12*a2*b22 - a3*b19 - 9*a3*b21 - 6*a4*b21 - 3*a5*b19 - 3
*a5*b21 + a6*b15 + 3*a6*b17 - 2*a6*b21 + 12*a7*b14 + 9*a7*b15 + 6*a7*b16 + 3*a7
*b17 + 6*a7*b20 + 6*a7*b21 + 12*a7*b22 - 4*a8*b11 - 16*a8*b12 - 120*a8*b13 - 6*
a9*b11 - 6*a9*b12 - 150*a9*b13 - 120*a9*b2 + 2*a9*b4 + a9*b5 - 2*a9*b7,
80*a1*b16 + 70*a1*b17 + 30*a1*b18 + 160*a1*b19 + 40*a1*b20 + 120*a1*b21 + 35*a1
*b22 - 8*a2*b8 + 2*a3*b11 + 2*a3*b12 + 2*a3*b9 - 8*a4*b10 + 2*a4*b11 + 2*a4*b12
 - 8*a4*b3 - 6*a5*b10 + 2*a5*b11 + 2*a5*b12 - 6*a5*b3 + 2*a5*b8 + 2*a5*b9 - 16*
a6*b10 - 16*a6*b3 - 4*a6*b9 - 12*a7*b10 - 12*a7*b3 - 3*a7*b9 - 840*a8*b1 - 1470
*a9*b1,
720*a1*b23 + 600*a1*b24 + 12*a2*b16 + 12*a2*b17 + 18*a2*b18 + 6*a2*b19 + 12*a2*
b20 + 15*a2*b22 - 2*a3*b16 - 3*a3*b17 + 2*a4*b15 - 4*a4*b17 + 3*a5*b15 + 4*a5*
b16 + 4*a5*b19 + 4*a5*b20 + 5*a5*b22 - 4*a6*b17 - 48*a8*b10 - 240*a8*b2 - 12*a8
*b5 - 8*a8*b8 - 12*a8*b9 - 78*a9*b10 - 300*a9*b2 - 9*a9*b5 - 2*a9*b6 - 10*a9*b8
 - 3*a9*b9,
360*a1*b23 + 300*a1*b24 + 12*a2*b16 + 6*a2*b17 + 6*a2*b18 + 12*a2*b19 + 6*a2*
b20 + 3*a2*b22 + 2*a3*b16 + 2*a3*b19 - 2*a4*b15 - 2*a4*b17 + 2*a4*b19 + 2*a5*
b16 + 6*a5*b19 + 2*a5*b20 + a5*b22 - 2*a6*b15 - 2*a6*b16 - 2*a6*b17 - 2*a6*b18 
- 12*a8*b10 - 120*a8*b2 - 12*a8*b3 - 16*a8*b8 - 42*a9*b10 - 150*a9*b2 - 12*a9*
b3 - 2*a9*b8 - 3*a9*b9,
720*a1*b23 + 600*a1*b24 + 4*a3*b16 + 2*a3*b17 + 2*a3*b18 + 2*a3*b19 + 2*a3*b20 
+ a3*b22 + 2*a4*b15 - 2*a4*b18 + 2*a4*b19 + 2*a4*b20 + a4*b22 + 4*a5*b16 + 2*a5
*b17 + 2*a5*b18 + 2*a5*b19 + 2*a5*b20 + a5*b22 - 2*a6*b18 - 48*a8*b10 - 48*a8*
b3 - 4*a8*b6 - 8*a8*b8 - 12*a8*b9 - 48*a9*b10 - 48*a9*b3 - 2*a9*b6 - 4*a9*b8 - 
15*a9*b9,
240*a1*b24 + 4*a2*b19 + 6*a2*b20 + 6*a2*b21 + 9*a2*b22 - 2*a3*b19 - 4*a3*b21 - 
6*a4*b21 - 6*a5*b21 + 4*a6*b14 + 2*a6*b15 - 2*a6*b21 - a6*b22 + 4*a7*b15 + 6*a7
*b16 + 6*a7*b17 + 8*a7*b19 + 6*a7*b20 + 6*a7*b21 + 9*a7*b22 - 4*a8*b11 - 24*a8*
b12 - 80*a8*b13 - 6*a9*b11 - 4*a9*b12 - 160*a9*b13 - 120*a9*b2 - 3*a9*b5 + a9*
b6 + a9*b7,
240*a1*b23 + 200*a1*b24 + 4*a2*b16 + 6*a2*b17 + 3*a2*b18 + 6*a2*b19 + 3*a2*b20 
+ 6*a2*b21 + 3*a2*b22 + a3*b17 + a3*b19 + a3*b21 + 4*a4*b14 - a4*b17 + a4*b19 +
 a4*b21 - a5*b15 + a5*b16 + 3*a5*b19 + a5*b20 + 3*a5*b21 + a5*b22 - a6*b15 - a6
*b16 - a6*b17 - a6*b18 - a7*b15 - a7*b16 - a7*b17 - a7*b18 - 8*a8*b10 - 80*a8*
b2 - 8*a8*b3 - 8*a8*b9 - 28*a9*b10 - 100*a9*b2 - 8*a9*b3 - 3*a9*b9

Computing time

On a Pentium 4 PC with 1.7GHz running REDUCE 3.7 with 120MB RAM under Linux the problem was solved in 408 sec.