18.783 Lecture 2 Proof of associativity.sagews

For affine points $P_1=(x_1,y_1,1)$ and $P_2=(x_2,y_2,1)$ the sum $P_1+P_2=P_3=(x_3,y_3,1)\ne 0$ is computed via:

$m = \frac{y_2-y_1}{x_2-x_1}$   (if $x_1\ne x_2$)      $m = \frac{3x_1^2+A}{2y_1}$    (if $x_1=x_2$)

$x_3 = m^2 - x_1 - x_2$;

$y_3 = m(x_3-x_1) + y_1$.

Let's verify that this operation is associative, i.e. $(P+Q)+R=P+(Q+R)$

Note that the equations are independent of the curve parameters, but we will need to use the fact that the points all satisfy the curve equation

$y^2=x^3 + Ax+B$.

RR.<Px,Py,Qx,Qy,Rx,Ry,A,B> = PolynomialRing(QQ,8)
# represent projective points on E uniquely, as either affine points (x,y,1) or the point O=(0,1,0) at infinity
P=(Px,Py,1); Q=(Qx,Qy,1); R=(Rx,Ry,1); O=(0,1,0);
I=RR.ideal(Py^2-Px^3-A*Px-B, Qy^2-Qx^3-A*Qx-B, Ry^2-Rx^3-A*Rx-B)
SS=RR.quotient(I)

def add(P,Q):
    """ general addition algorithm for an elliptic curve in short Weierstrass form"""
    if P == O: return Q
    if Q == O: return P
    assert P[2] == 1 and Q[2] == 1  # we are using affine formulas, so make sure points are in affine form
    x1=P[0]; y1=P[1]; x2=Q[0]; y2=Q[1];
    if x1 != x2:
        m = (y2-y1)/(x2-x1)         # usual case: P and Q are distinct and not opposites
    else:
        if y1 == -y2: return O      # P = -Q (includes case where P=Q is 2-torsion)
        m = (3*x1^2+A) / (2*y1)     # P = Q so we are doubling
    x3 = m^2-x1-x2
    y3 = m*(x1-x3)-y1
    return (x3,y3,1)

def negate(P):
    if P == O: return O
    return (P[0],-P[1],P[2])
    
def reduced_fractions_equal(p,q):
    return SS(p.numerator()*q.denominator()-p.denominator()*q.numerator()) == 0
    
def on_curve(P):
    return reduced_fractions_equal(P[1]^2*P[2],P[0]^3+A*P[0]*P[2]^2+B*P[2]^3)
    
def equal(P,Q):
    return reduced_fractions_equal(P[0]*Q[2],Q[0]*P[2]) and reduced_fractions_equal(P[1]*Q[2],Q[1]*P[2])

As a sanity check, let's first verify that the output of add($P$,$Q$) is always on the curve, and check the identity, inverses, and commutativity

print on_curve(O) and on_curve(negate(P)) and on_curve(add(P,Q)) and on_curve(add(P,P)) and on_curve(add(P,negate(P)))
print add(P,O) == P and add(O,P) == P
print add(P,negate(P)) == O
print add(P,Q) == add(Q,P)

True True True True

Good, now for associativity in the general case...

add(add(P,Q),R) == add(P,add(Q,R))

False

Oops, we forgot to use the curve equation, we need to use our "equal" function which reduces into the quotient ring.

equal(add(add(P,Q),R),add(P,add(Q,R)))

True

Now check the cases where 2 points are equal,

equal(add(add(P,P),Q),add(P,add(P,Q))) and equal(add(add(P,Q),P),add(P,add(Q,P))) and equal(add(add(Q,P),P),add(Q,add(P,P)))

True

and also cases where 2 points are opposites,

S = negate(P);
equal(add(add(P,S),Q),add(P,add(S,Q))) and equal(add(add(P,Q),S),add(P,add(Q,S))) and equal(add(add(Q,P),S),add(Q,add(P,S)))

True

and when all 3 points are equal

equal(add(add(P,P),P),add(P,add(P,P)))

True

Just to be paranoid, also check cases where R is P+Q, P-Q, or -(P+Q),

equal(add(add(P,Q),add(P,Q)),add(P,add(Q,add(P,Q)))) and equal(add(add(P,Q),add(P,negate(Q))),add(P,add(Q,add(P,negate(Q))))) and equal(add(add(P,Q),negate(add(P,Q))),add(P,add(Q,negate(add(P,Q)))))

True

and cases where R is 2P or -2P

equal(add(add(P,Q),add(P,P)),add(P,add(Q,add(P,P)))) and equal(add(add(P,Q),negate(add(P,P))),add(P,add(Q,negate(add(P,P)))))

True

Just in case this all looked too easy, take a look at what is actually being compared...

print add(add(P,Q),R), "\n\n    versus   \n\n", add(P,add(Q,R))

((Px^7 - Px^6*Qx - 3*Px^5*Qx^2 + 3*Px^4*Qx^3 + 3*Px^3*Qx^4 - 3*Px^2*Qx^5 - Px*Qx^6 + Qx^7 + Px^6*Rx - 2*Px^5*Qx*Rx - Px^4*Qx^2*Rx + 4*Px^3*Qx^3*Rx - Px^2*Qx^4*Rx - 2*Px*Qx^5*Rx + Qx^6*Rx - Px^5*Rx^2 + 3*Px^4*Qx*Rx^2 - 2*Px^3*Qx^2*Rx^2 - 2*Px^2*Qx^3*Rx^2 + 3*Px*Qx^4*Rx^2 - Qx^5*Rx^2 - Px^4*Rx^3 + 4*Px^3*Qx*Rx^3 - 6*Px^2*Qx^2*Rx^3 + 4*Px*Qx^3*Rx^3 - Qx^4*Rx^3 - 2*Px^4*Py^2 + 2*Px^3*Py^2*Qx + 3*Px^2*Py^2*Qx^2 - 4*Px*Py^2*Qx^3 + Py^2*Qx^4 + 2*Px^4*Py*Qy - 2*Px^3*Py*Qx*Qy - 2*Px*Py*Qx^3*Qy + 2*Py*Qx^4*Qy + Px^4*Qy^2 - 4*Px^3*Qx*Qy^2 + 3*Px^2*Qx^2*Qy^2 + 2*Px*Qx^3*Qy^2 - 2*Qx^4*Qy^2 - 2*Px^3*Py^2*Rx + 2*Px^2*Py^2*Qx*Rx + 2*Px*Py^2*Qx^2*Rx - 2*Py^2*Qx^3*Rx + 4*Px^3*Py*Qy*Rx - 4*Px^2*Py*Qx*Qy*Rx - 4*Px*Py*Qx^2*Qy*Rx + 4*Py*Qx^3*Qy*Rx - 2*Px^3*Qy^2*Rx + 2*Px^2*Qx*Qy^2*Rx + 2*Px*Qx^2*Qy^2*Rx - 2*Qx^3*Qy^2*Rx + Px^2*Py^2*Rx^2 - 2*Px*Py^2*Qx*Rx^2 + Py^2*Qx^2*Rx^2 - 2*Px^2*Py*Qy*Rx^2 + 4*Px*Py*Qx*Qy*Rx^2 - 2*Py*Qx^2*Qy*Rx^2 + Px^2*Qy^2*Rx^2 - 2*Px*Qx*Qy^2*Rx^2 + Qx^2*Qy^2*Rx^2 - 2*Px^4*Py*Ry + 2*Px^3*Py*Qx*Ry + 6*Px^2*Py*Qx^2*Ry - 10*Px*Py*Qx^3*Ry + 4*Py*Qx^4*Ry + 4*Px^4*Qy*Ry - 10*Px^3*Qx*Qy*Ry + 6*Px^2*Qx^2*Qy*Ry + 2*Px*Qx^3*Qy*Ry - 2*Qx^4*Qy*Ry + Px^4*Ry^2 - 4*Px^3*Qx*Ry^2 + 6*Px^2*Qx^2*Ry^2 - 4*Px*Qx^3*Ry^2 + Qx^4*Ry^2 + Px*Py^4 - Py^4*Qx - 2*Px*Py^3*Qy + 2*Py^3*Qx*Qy + 2*Px*Py*Qy^3 - 2*Py*Qx*Qy^3 - Px*Qy^4 + Qx*Qy^4 + Py^4*Rx - 4*Py^3*Qy*Rx + 6*Py^2*Qy^2*Rx - 4*Py*Qy^3*Rx + Qy^4*Rx + 2*Px*Py^3*Ry - 2*Py^3*Qx*Ry - 6*Px*Py^2*Qy*Ry + 6*Py^2*Qx*Qy*Ry + 6*Px*Py*Qy^2*Ry - 6*Py*Qx*Qy^2*Ry - 2*Px*Qy^3*Ry + 2*Qx*Qy^3*Ry)/(Px^6 - 2*Px^5*Qx - Px^4*Qx^2 + 4*Px^3*Qx^3 - Px^2*Qx^4 - 2*Px*Qx^5 + Qx^6 + 2*Px^5*Rx - 6*Px^4*Qx*Rx + 4*Px^3*Qx^2*Rx + 4*Px^2*Qx^3*Rx - 6*Px*Qx^4*Rx + 2*Qx^5*Rx + Px^4*Rx^2 - 4*Px^3*Qx*Rx^2 + 6*Px^2*Qx^2*Rx^2 - 4*Px*Qx^3*Rx^2 + Qx^4*Rx^2 - 2*Px^3*Py^2 + 2*Px^2*Py^2*Qx + 2*Px*Py^2*Qx^2 - 2*Py^2*Qx^3 + 4*Px^3*Py*Qy - 4*Px^2*Py*Qx*Qy - 4*Px*Py*Qx^2*Qy + 4*Py*Qx^3*Qy - 2*Px^3*Qy^2 + 2*Px^2*Qx*Qy^2 + 2*Px*Qx^2*Qy^2 - 2*Qx^3*Qy^2 - 2*Px^2*Py^2*Rx + 4*Px*Py^2*Qx*Rx - 2*Py^2*Qx^2*Rx + 4*Px^2*Py*Qy*Rx - 8*Px*Py*Qx*Qy*Rx + 4*Py*Qx^2*Qy*Rx - 2*Px^2*Qy^2*Rx + 4*Px*Qx*Qy^2*Rx - 2*Qx^2*Qy^2*Rx + Py^4 - 4*Py^3*Qy + 6*Py^2*Qy^2 - 4*Py*Qy^3 + Qy^4), (Px^9*Py - 6*Px^7*Py*Qx^2 + 2*Px^6*Py*Qx^3 + 12*Px^5*Py*Qx^4 - 6*Px^4*Py*Qx^5 - 10*Px^3*Py*Qx^6 + 6*Px^2*Py*Qx^7 + 3*Px*Py*Qx^8 - 2*Py*Qx^9 - 2*Px^9*Qy + 3*Px^8*Qx*Qy + 6*Px^7*Qx^2*Qy - 10*Px^6*Qx^3*Qy - 6*Px^5*Qx^4*Qy + 12*Px^4*Qx^5*Qy + 2*Px^3*Qx^6*Qy - 6*Px^2*Qx^7*Qy + Qx^9*Qy - 3*Px^7*Py*Rx^2 + 6*Px^6*Py*Qx*Rx^2 + 9*Px^5*Py*Qx^2*Rx^2 - 30*Px^4*Py*Qx^3*Rx^2 + 15*Px^3*Py*Qx^4*Rx^2 + 18*Px^2*Py*Qx^5*Rx^2 - 21*Px*Py*Qx^6*Rx^2 + 6*Py*Qx^7*Rx^2 + 6*Px^7*Qy*Rx^2 - 21*Px^6*Qx*Qy*Rx^2 + 18*Px^5*Qx^2*Qy*Rx^2 + 15*Px^4*Qx^3*Qy*Rx^2 - 30*Px^3*Qx^4*Qy*Rx^2 + 9*Px^2*Qx^5*Qy*Rx^2 + 6*Px*Qx^6*Qy*Rx^2 - 3*Qx^7*Qy*Rx^2 - 2*Px^6*Py*Rx^3 + 6*Px^5*Py*Qx*Rx^3 - 20*Px^3*Py*Qx^3*Rx^3 + 30*Px^2*Py*Qx^4*Rx^3 - 18*Px*Py*Qx^5*Rx^3 + 4*Py*Qx^6*Rx^3 + 4*Px^6*Qy*Rx^3 - 18*Px^5*Qx*Qy*Rx^3 + 30*Px^4*Qx^2*Qy*Rx^3 - 20*Px^3*Qx^3*Qy*Rx^3 + 6*Px*Qx^5*Qy*Rx^3 - 2*Qx^6*Qy*Rx^3 - 2*Px^9*Ry + 6*Px^8*Qx*Ry - 16*Px^6*Qx^3*Ry + 12*Px^5*Qx^4*Ry + 12*Px^4*Qx^5*Ry - 16*Px^3*Qx^6*Ry + 6*Px*Qx^8*Ry - 2*Qx^9*Ry - 3*Px^8*Rx*Ry + 12*Px^7*Qx*Rx*Ry - 12*Px^6*Qx^2*Rx*Ry - 12*Px^5*Qx^3*Rx*Ry + 30*Px^4*Qx^4*Rx*Ry - 12*Px^3*Qx^5*Rx*Ry - 12*Px^2*Qx^6*Rx*Ry + 12*Px*Qx^7*Rx*Ry - 3*Qx^8*Rx*Ry + Px^6*Rx^3*Ry - 6*Px^5*Qx*Rx^3*Ry + 15*Px^4*Qx^2*Rx^3*Ry - 20*Px^3*Qx^3*Rx^3*Ry + 15*Px^2*Qx^4*Rx^3*Ry - 6*Px*Qx^5*Rx^3*Ry + Qx^6*Rx^3*Ry - 3*Px^6*Py^3 + 12*Px^4*Py^3*Qx^2 - 5*Px^3*Py^3*Qx^3 - 12*Px^2*Py^3*Qx^4 + 9*Px*Py^3*Qx^5 - Py^3*Qx^6 + 9*Px^6*Py^2*Qy - 6*Px^5*Py^2*Qx*Qy - 21*Px^4*Py^2*Qx^2*Qy + 15*Px^3*Py^2*Qx^3*Qy + 6*Px^2*Py^2*Qx^4*Qy + 3*Px*Py^2*Qx^5*Qy - 6*Py^2*Qx^6*Qy - 6*Px^6*Py*Qy^2 + 3*Px^5*Py*Qx*Qy^2 + 6*Px^4*Py*Qx^2*Qy^2 + 15*Px^3*Py*Qx^3*Qy^2 - 21*Px^2*Py*Qx^4*Qy^2 - 6*Px*Py*Qx^5*Qy^2 + 9*Py*Qx^6*Qy^2 - Px^6*Qy^3 + 9*Px^5*Qx*Qy^3 - 12*Px^4*Qx^2*Qy^3 - 5*Px^3*Qx^3*Qy^3 + 12*Px^2*Qx^4*Qy^3 - 3*Qx^6*Qy^3 + 6*Px^4*Py^3*Rx^2 - 9*Px^3*Py^3*Qx*Rx^2 - 9*Px^2*Py^3*Qx^2*Rx^2 + 21*Px*Py^3*Qx^3*Rx^2 - 9*Py^3*Qx^4*Rx^2 - 21*Px^4*Py^2*Qy*Rx^2 + 39*Px^3*Py^2*Qx*Qy*Rx^2 + 9*Px^2*Py^2*Qx^2*Qy*Rx^2 - 51*Px*Py^2*Qx^3*Qy*Rx^2 + 24*Py^2*Qx^4*Qy*Rx^2 + 24*Px^4*Py*Qy^2*Rx^2 - 51*Px^3*Py*Qx*Qy^2*Rx^2 + 9*Px^2*Py*Qx^2*Qy^2*Rx^2 + 39*Px*Py*Qx^3*Qy^2*Rx^2 - 21*Py*Qx^4*Qy^2*Rx^2 - 9*Px^4*Qy^3*Rx^2 + 21*Px^3*Qx*Qy^3*Rx^2 - 9*Px^2*Qx^2*Qy^3*Rx^2 - 9*Px*Qx^3*Qy^3*Rx^2 + 6*Qx^4*Qy^3*Rx^2 + 2*Px^3*Py^3*Rx^3 - 6*Px^2*Py^3*Qx*Rx^3 + 6*Px*Py^3*Qx^2*Rx^3 - 2*Py^3*Qx^3*Rx^3 - 6*Px^3*Py^2*Qy*Rx^3 + 18*Px^2*Py^2*Qx*Qy*Rx^3 - 18*Px*Py^2*Qx^2*Qy*Rx^3 + 6*Py^2*Qx^3*Qy*Rx^3 + 6*Px^3*Py*Qy^2*Rx^3 - 18*Px^2*Py*Qx*Qy^2*Rx^3 + 18*Px*Py*Qx^2*Qy^2*Rx^3 - 6*Py*Qx^3*Qy^2*Rx^3 - 2*Px^3*Qy^3*Rx^3 + 6*Px^2*Qx*Qy^3*Rx^3 - 6*Px*Qx^2*Qy^3*Rx^3 + 2*Qx^3*Qy^3*Rx^3 + 3*Px^6*Py^2*Ry - 12*Px^5*Py^2*Qx*Ry + 12*Px^4*Py^2*Qx^2*Ry + 12*Px^3*Py^2*Qx^3*Ry - 33*Px^2*Py^2*Qx^4*Ry + 24*Px*Py^2*Qx^5*Ry - 6*Py^2*Qx^6*Ry + 6*Px^5*Py*Qx*Qy*Ry - 24*Px^4*Py*Qx^2*Qy*Ry + 36*Px^3*Py*Qx^3*Qy*Ry - 24*Px^2*Py*Qx^4*Qy*Ry + 6*Px*Py*Qx^5*Qy*Ry - 6*Px^6*Qy^2*Ry + 24*Px^5*Qx*Qy^2*Ry - 33*Px^4*Qx^2*Qy^2*Ry + 12*Px^3*Qx^3*Qy^2*Ry + 12*Px^2*Qx^4*Qy^2*Ry - 12*Px*Qx^5*Qy^2*Ry + 3*Qx^6*Qy^2*Ry + 6*Px^5*Py^2*Rx*Ry - 18*Px^4*Py^2*Qx*Rx*Ry + 12*Px^3*Py^2*Qx^2*Rx*Ry + 12*Px^2*Py^2*Qx^3*Rx*Ry - 18*Px*Py^2*Qx^4*Rx*Ry + 6*Py^2*Qx^5*Rx*Ry - 12*Px^5*Py*Qy*Rx*Ry + 36*Px^4*Py*Qx*Qy*Rx*Ry - 24*Px^3*Py*Qx^2*Qy*Rx*Ry - 24*Px^2*Py*Qx^3*Qy*Rx*Ry + 36*Px*Py*Qx^4*Qy*Rx*Ry - 12*Py*Qx^5*Qy*Rx*Ry + 6*Px^5*Qy^2*Rx*Ry - 18*Px^4*Qx*Qy^2*Rx*Ry + 12*Px^3*Qx^2*Qy^2*Rx*Ry + 12*Px^2*Qx^3*Qy^2*Rx*Ry - 18*Px*Qx^4*Qy^2*Rx*Ry + 6*Qx^5*Qy^2*Rx*Ry + 3*Px^6*Py*Ry^2 - 9*Px^5*Py*Qx*Ry^2 + 30*Px^3*Py*Qx^3*Ry^2 - 45*Px^2*Py*Qx^4*Ry^2 + 27*Px*Py*Qx^5*Ry^2 - 6*Py*Qx^6*Ry^2 - 6*Px^6*Qy*Ry^2 + 27*Px^5*Qx*Qy*Ry^2 - 45*Px^4*Qx^2*Qy*Ry^2 + 30*Px^3*Qx^3*Qy*Ry^2 - 9*Px*Qx^5*Qy*Ry^2 + 3*Qx^6*Qy*Ry^2 - Px^6*Ry^3 + 6*Px^5*Qx*Ry^3 - 15*Px^4*Qx^2*Ry^3 + 20*Px^3*Qx^3*Ry^3 - 15*Px^2*Qx^4*Ry^3 + 6*Px*Qx^5*Ry^3 - Qx^6*Ry^3 + 3*Px^3*Py^5 - 6*Px*Py^5*Qx^2 + 3*Py^5*Qx^3 - 12*Px^3*Py^4*Qy + 3*Px^2*Py^4*Qx*Qy + 15*Px*Py^4*Qx^2*Qy - 6*Py^4*Qx^3*Qy + 15*Px^3*Py^3*Qy^2 - 3*Px^2*Py^3*Qx*Qy^2 - 9*Px*Py^3*Qx^2*Qy^2 - 3*Py^3*Qx^3*Qy^2 - 3*Px^3*Py^2*Qy^3 - 9*Px^2*Py^2*Qx*Qy^3 - 3*Px*Py^2*Qx^2*Qy^3 + 15*Py^2*Qx^3*Qy^3 - 6*Px^3*Py*Qy^4 + 15*Px^2*Py*Qx*Qy^4 + 3*Px*Py*Qx^2*Qy^4 - 12*Py*Qx^3*Qy^4 + 3*Px^3*Qy^5 - 6*Px^2*Qx*Qy^5 + 3*Qx^3*Qy^5 - 3*Px*Py^5*Rx^2 + 3*Py^5*Qx*Rx^2 + 15*Px*Py^4*Qy*Rx^2 - 15*Py^4*Qx*Qy*Rx^2 - 30*Px*Py^3*Qy^2*Rx^2 + 30*Py^3*Qx*Qy^2*Rx^2 + 30*Px*Py^2*Qy^3*Rx^2 - 30*Py^2*Qx*Qy^3*Rx^2 - 15*Px*Py*Qy^4*Rx^2 + 15*Py*Qx*Qy^4*Rx^2 + 3*Px*Qy^5*Rx^2 - 3*Qx*Qy^5*Rx^2 + 6*Px^2*Py^4*Qx*Ry - 12*Px*Py^4*Qx^2*Ry + 6*Py^4*Qx^3*Ry - 6*Px^3*Py^3*Qy*Ry - 6*Px^2*Py^3*Qx*Qy*Ry + 30*Px*Py^3*Qx^2*Qy*Ry - 18*Py^3*Qx^3*Qy*Ry + 18*Px^3*Py^2*Qy^2*Ry - 18*Px^2*Py^2*Qx*Qy^2*Ry - 18*Px*Py^2*Qx^2*Qy^2*Ry + 18*Py^2*Qx^3*Qy^2*Ry - 18*Px^3*Py*Qy^3*Ry + 30*Px^2*Py*Qx*Qy^3*Ry - 6*Px*Py*Qx^2*Qy^3*Ry - 6*Py*Qx^3*Qy^3*Ry + 6*Px^3*Qy^4*Ry - 12*Px^2*Qx*Qy^4*Ry + 6*Px*Qx^2*Qy^4*Ry - 3*Px^2*Py^4*Rx*Ry + 6*Px*Py^4*Qx*Rx*Ry - 3*Py^4*Qx^2*Rx*Ry + 12*Px^2*Py^3*Qy*Rx*Ry - 24*Px*Py^3*Qx*Qy*Rx*Ry + 12*Py^3*Qx^2*Qy*Rx*Ry - 18*Px^2*Py^2*Qy^2*Rx*Ry + 36*Px*Py^2*Qx*Qy^2*Rx*Ry - 18*Py^2*Qx^2*Qy^2*Rx*Ry + 12*Px^2*Py*Qy^3*Rx*Ry - 24*Px*Py*Qx*Qy^3*Rx*Ry + 12*Py*Qx^2*Qy^3*Rx*Ry - 3*Px^2*Qy^4*Rx*Ry + 6*Px*Qx*Qy^4*Rx*Ry - 3*Qx^2*Qy^4*Rx*Ry - 3*Px^3*Py^3*Ry^2 + 9*Px^2*Py^3*Qx*Ry^2 - 9*Px*Py^3*Qx^2*Ry^2 + 3*Py^3*Qx^3*Ry^2 + 9*Px^3*Py^2*Qy*Ry^2 - 27*Px^2*Py^2*Qx*Qy*Ry^2 + 27*Px*Py^2*Qx^2*Qy*Ry^2 - 9*Py^2*Qx^3*Qy*Ry^2 - 9*Px^3*Py*Qy^2*Ry^2 + 27*Px^2*Py*Qx*Qy^2*Ry^2 - 27*Px*Py*Qx^2*Qy^2*Ry^2 + 9*Py*Qx^3*Qy^2*Ry^2 + 3*Px^3*Qy^3*Ry^2 - 9*Px^2*Qx*Qy^3*Ry^2 + 9*Px*Qx^2*Qy^3*Ry^2 - 3*Qx^3*Qy^3*Ry^2 - Py^7 + 5*Py^6*Qy - 9*Py^5*Qy^2 + 5*Py^4*Qy^3 + 5*Py^3*Qy^4 - 9*Py^2*Qy^5 + 5*Py*Qy^6 - Qy^7 - Py^6*Ry + 6*Py^5*Qy*Ry - 15*Py^4*Qy^2*Ry + 20*Py^3*Qy^3*Ry - 15*Py^2*Qy^4*Ry + 6*Py*Qy^5*Ry - Qy^6*Ry)/(Px^9 - 3*Px^8*Qx + 8*Px^6*Qx^3 - 6*Px^5*Qx^4 - 6*Px^4*Qx^5 + 8*Px^3*Qx^6 - 3*Px*Qx^8 + Qx^9 + 3*Px^8*Rx - 12*Px^7*Qx*Rx + 12*Px^6*Qx^2*Rx + 12*Px^5*Qx^3*Rx - 30*Px^4*Qx^4*Rx + 12*Px^3*Qx^5*Rx + 12*Px^2*Qx^6*Rx - 12*Px*Qx^7*Rx + 3*Qx^8*Rx + 3*Px^7*Rx^2 - 15*Px^6*Qx*Rx^2 + 27*Px^5*Qx^2*Rx^2 - 15*Px^4*Qx^3*Rx^2 - 15*Px^3*Qx^4*Rx^2 + 27*Px^2*Qx^5*Rx^2 - 15*Px*Qx^6*Rx^2 + 3*Qx^7*Rx^2 + Px^6*Rx^3 - 6*Px^5*Qx*Rx^3 + 15*Px^4*Qx^2*Rx^3 - 20*Px^3*Qx^3*Rx^3 + 15*Px^2*Qx^4*Rx^3 - 6*Px*Qx^5*Rx^3 + Qx^6*Rx^3 - 3*Px^6*Py^2 + 6*Px^5*Py^2*Qx + 3*Px^4*Py^2*Qx^2 - 12*Px^3*Py^2*Qx^3 + 3*Px^2*Py^2*Qx^4 + 6*Px*Py^2*Qx^5 - 3*Py^2*Qx^6 + 6*Px^6*Py*Qy - 12*Px^5*Py*Qx*Qy - 6*Px^4*Py*Qx^2*Qy + 24*Px^3*Py*Qx^3*Qy - 6*Px^2*Py*Qx^4*Qy - 12*Px*Py*Qx^5*Qy + 6*Py*Qx^6*Qy - 3*Px^6*Qy^2 + 6*Px^5*Qx*Qy^2 + 3*Px^4*Qx^2*Qy^2 - 12*Px^3*Qx^3*Qy^2 + 3*Px^2*Qx^4*Qy^2 + 6*Px*Qx^5*Qy^2 - 3*Qx^6*Qy^2 - 6*Px^5*Py^2*Rx + 18*Px^4*Py^2*Qx*Rx - 12*Px^3*Py^2*Qx^2*Rx - 12*Px^2*Py^2*Qx^3*Rx + 18*Px*Py^2*Qx^4*Rx - 6*Py^2*Qx^5*Rx + 12*Px^5*Py*Qy*Rx - 36*Px^4*Py*Qx*Qy*Rx + 24*Px^3*Py*Qx^2*Qy*Rx + 24*Px^2*Py*Qx^3*Qy*Rx - 36*Px*Py*Qx^4*Qy*Rx + 12*Py*Qx^5*Qy*Rx - 6*Px^5*Qy^2*Rx + 18*Px^4*Qx*Qy^2*Rx - 12*Px^3*Qx^2*Qy^2*Rx - 12*Px^2*Qx^3*Qy^2*Rx + 18*Px*Qx^4*Qy^2*Rx - 6*Qx^5*Qy^2*Rx - 3*Px^4*Py^2*Rx^2 + 12*Px^3*Py^2*Qx*Rx^2 - 18*Px^2*Py^2*Qx^2*Rx^2 + 12*Px*Py^2*Qx^3*Rx^2 - 3*Py^2*Qx^4*Rx^2 + 6*Px^4*Py*Qy*Rx^2 - 24*Px^3*Py*Qx*Qy*Rx^2 + 36*Px^2*Py*Qx^2*Qy*Rx^2 - 24*Px*Py*Qx^3*Qy*Rx^2 + 6*Py*Qx^4*Qy*Rx^2 - 3*Px^4*Qy^2*Rx^2 + 12*Px^3*Qx*Qy^2*Rx^2 - 18*Px^2*Qx^2*Qy^2*Rx^2 + 12*Px*Qx^3*Qy^2*Rx^2 - 3*Qx^4*Qy^2*Rx^2 + 3*Px^3*Py^4 - 3*Px^2*Py^4*Qx - 3*Px*Py^4*Qx^2 + 3*Py^4*Qx^3 - 12*Px^3*Py^3*Qy + 12*Px^2*Py^3*Qx*Qy + 12*Px*Py^3*Qx^2*Qy - 12*Py^3*Qx^3*Qy + 18*Px^3*Py^2*Qy^2 - 18*Px^2*Py^2*Qx*Qy^2 - 18*Px*Py^2*Qx^2*Qy^2 + 18*Py^2*Qx^3*Qy^2 - 12*Px^3*Py*Qy^3 + 12*Px^2*Py*Qx*Qy^3 + 12*Px*Py*Qx^2*Qy^3 - 12*Py*Qx^3*Qy^3 + 3*Px^3*Qy^4 - 3*Px^2*Qx*Qy^4 - 3*Px*Qx^2*Qy^4 + 3*Qx^3*Qy^4 + 3*Px^2*Py^4*Rx - 6*Px*Py^4*Qx*Rx + 3*Py^4*Qx^2*Rx - 12*Px^2*Py^3*Qy*Rx + 24*Px*Py^3*Qx*Qy*Rx - 12*Py^3*Qx^2*Qy*Rx + 18*Px^2*Py^2*Qy^2*Rx - 36*Px*Py^2*Qx*Qy^2*Rx + 18*Py^2*Qx^2*Qy^2*Rx - 12*Px^2*Py*Qy^3*Rx + 24*Px*Py*Qx*Qy^3*Rx - 12*Py*Qx^2*Qy^3*Rx + 3*Px^2*Qy^4*Rx - 6*Px*Qx*Qy^4*Rx + 3*Qx^2*Qy^4*Rx - Py^6 + 6*Py^5*Qy - 15*Py^4*Qy^2 + 20*Py^3*Qy^3 - 15*Py^2*Qy^4 + 6*Py*Qy^5 - Qy^6), 1) versus ((-Px^3*Qx^4 - Px^2*Qx^5 + Px*Qx^6 + Qx^7 + 4*Px^3*Qx^3*Rx + 3*Px^2*Qx^4*Rx - 2*Px*Qx^5*Rx - Qx^6*Rx - 6*Px^3*Qx^2*Rx^2 - 2*Px^2*Qx^3*Rx^2 - Px*Qx^4*Rx^2 - 3*Qx^5*Rx^2 + 4*Px^3*Qx*Rx^3 - 2*Px^2*Qx^2*Rx^3 + 4*Px*Qx^3*Rx^3 + 3*Qx^4*Rx^3 - Px^3*Rx^4 + 3*Px^2*Qx*Rx^4 - Px*Qx^2*Rx^4 + 3*Qx^3*Rx^4 - Px^2*Rx^5 - 2*Px*Qx*Rx^5 - 3*Qx^2*Rx^5 + Px*Rx^6 - Qx*Rx^6 + Rx^7 + Py^2*Qx^4 - 2*Py*Qx^4*Qy + Px^2*Qx^2*Qy^2 - 2*Px*Qx^3*Qy^2 - 2*Qx^4*Qy^2 - 4*Py^2*Qx^3*Rx + 2*Py*Qx^3*Qy*Rx - 2*Px^2*Qx*Qy^2*Rx + 2*Px*Qx^2*Qy^2*Rx + 2*Qx^3*Qy^2*Rx + 6*Py^2*Qx^2*Rx^2 + 6*Py*Qx^2*Qy*Rx^2 + Px^2*Qy^2*Rx^2 + 2*Px*Qx*Qy^2*Rx^2 + 3*Qx^2*Qy^2*Rx^2 - 4*Py^2*Qx*Rx^3 - 10*Py*Qx*Qy*Rx^3 - 2*Px*Qy^2*Rx^3 - 4*Qx*Qy^2*Rx^3 + Py^2*Rx^4 + 4*Py*Qy*Rx^4 + Qy^2*Rx^4 + 4*Py*Qx^4*Ry - 2*Px^2*Qx^2*Qy*Ry + 4*Px*Qx^3*Qy*Ry + 2*Qx^4*Qy*Ry - 10*Py*Qx^3*Rx*Ry + 4*Px^2*Qx*Qy*Rx*Ry - 4*Px*Qx^2*Qy*Rx*Ry - 2*Qx^3*Qy*Rx*Ry + 6*Py*Qx^2*Rx^2*Ry - 2*Px^2*Qy*Rx^2*Ry - 4*Px*Qx*Qy*Rx^2*Ry + 2*Py*Qx*Rx^3*Ry + 4*Px*Qy*Rx^3*Ry - 2*Qx*Qy*Rx^3*Ry - 2*Py*Rx^4*Ry + 2*Qy*Rx^4*Ry + Px^2*Qx^2*Ry^2 - 2*Px*Qx^3*Ry^2 + Qx^4*Ry^2 - 2*Px^2*Qx*Rx*Ry^2 + 2*Px*Qx^2*Rx*Ry^2 - 4*Qx^3*Rx*Ry^2 + Px^2*Rx^2*Ry^2 + 2*Px*Qx*Rx^2*Ry^2 + 3*Qx^2*Rx^2*Ry^2 - 2*Px*Rx^3*Ry^2 + 2*Qx*Rx^3*Ry^2 - 2*Rx^4*Ry^2 + 2*Py*Qx*Qy^3 + Px*Qy^4 + Qx*Qy^4 - 2*Py*Qy^3*Rx - Qy^4*Rx - 6*Py*Qx*Qy^2*Ry - 4*Px*Qy^3*Ry - 2*Qx*Qy^3*Ry + 6*Py*Qy^2*Rx*Ry + 2*Qy^3*Rx*Ry + 6*Py*Qx*Qy*Ry^2 + 6*Px*Qy^2*Ry^2 - 6*Py*Qy*Rx*Ry^2 - 2*Py*Qx*Ry^3 - 4*Px*Qy*Ry^3 + 2*Qx*Qy*Ry^3 + 2*Py*Rx*Ry^3 - 2*Qy*Rx*Ry^3 + Px*Ry^4 - Qx*Ry^4 + Rx*Ry^4)/(Px^2*Qx^4 + 2*Px*Qx^5 + Qx^6 - 4*Px^2*Qx^3*Rx - 6*Px*Qx^4*Rx - 2*Qx^5*Rx + 6*Px^2*Qx^2*Rx^2 + 4*Px*Qx^3*Rx^2 - Qx^4*Rx^2 - 4*Px^2*Qx*Rx^3 + 4*Px*Qx^2*Rx^3 + 4*Qx^3*Rx^3 + Px^2*Rx^4 - 6*Px*Qx*Rx^4 - Qx^2*Rx^4 + 2*Px*Rx^5 - 2*Qx*Rx^5 + Rx^6 - 2*Px*Qx^2*Qy^2 - 2*Qx^3*Qy^2 + 4*Px*Qx*Qy^2*Rx + 2*Qx^2*Qy^2*Rx - 2*Px*Qy^2*Rx^2 + 2*Qx*Qy^2*Rx^2 - 2*Qy^2*Rx^3 + 4*Px*Qx^2*Qy*Ry + 4*Qx^3*Qy*Ry - 8*Px*Qx*Qy*Rx*Ry - 4*Qx^2*Qy*Rx*Ry + 4*Px*Qy*Rx^2*Ry - 4*Qx*Qy*Rx^2*Ry + 4*Qy*Rx^3*Ry - 2*Px*Qx^2*Ry^2 - 2*Qx^3*Ry^2 + 4*Px*Qx*Rx*Ry^2 + 2*Qx^2*Rx*Ry^2 - 2*Px*Rx^2*Ry^2 + 2*Qx*Rx^2*Ry^2 - 2*Rx^3*Ry^2 + Qy^4 - 4*Qy^3*Ry + 6*Qy^2*Ry^2 - 4*Qy*Ry^3 + Ry^4), (-Px^3*Py*Qx^6 + 3*Px*Py*Qx^8 + 2*Py*Qx^9 + 2*Px^3*Qx^6*Qy + 3*Px^2*Qx^7*Qy - Qx^9*Qy + 6*Px^3*Py*Qx^5*Rx - 12*Px*Py*Qx^7*Rx - 6*Py*Qx^8*Rx - 6*Px^3*Qx^5*Qy*Rx - 6*Px^2*Qx^6*Qy*Rx - 15*Px^3*Py*Qx^4*Rx^2 + 12*Px*Py*Qx^6*Rx^2 - 9*Px^2*Qx^5*Qy*Rx^2 + 6*Qx^7*Qy*Rx^2 + 20*Px^3*Py*Qx^3*Rx^3 + 12*Px*Py*Qx^5*Rx^3 + 16*Py*Qx^6*Rx^3 + 20*Px^3*Qx^3*Qy*Rx^3 + 30*Px^2*Qx^4*Qy*Rx^3 - 2*Qx^6*Qy*Rx^3 - 15*Px^3*Py*Qx^2*Rx^4 - 30*Px*Py*Qx^4*Rx^4 - 12*Py*Qx^5*Rx^4 - 30*Px^3*Qx^2*Qy*Rx^4 - 15*Px^2*Qx^3*Qy*Rx^4 - 12*Qx^5*Qy*Rx^4 + 6*Px^3*Py*Qx*Rx^5 + 12*Px*Py*Qx^3*Rx^5 - 12*Py*Qx^4*Rx^5 + 18*Px^3*Qx*Qy*Rx^5 - 18*Px^2*Qx^2*Qy*Rx^5 + 6*Qx^4*Qy*Rx^5 - Px^3*Py*Rx^6 + 12*Px*Py*Qx^2*Rx^6 + 16*Py*Qx^3*Rx^6 - 4*Px^3*Qy*Rx^6 + 21*Px^2*Qx*Qy*Rx^6 + 10*Qx^3*Qy*Rx^6 - 12*Px*Py*Qx*Rx^7 - 6*Px^2*Qy*Rx^7 - 6*Qx^2*Qy*Rx^7 + 3*Px*Py*Rx^8 - 6*Py*Qx*Rx^8 - 3*Qx*Qy*Rx^8 + 2*Py*Rx^9 + 2*Qy*Rx^9 - 4*Px^3*Qx^6*Ry - 6*Px^2*Qx^7*Ry + 2*Qx^9*Ry + 18*Px^3*Qx^5*Rx*Ry + 21*Px^2*Qx^6*Rx*Ry - 3*Qx^8*Rx*Ry - 30*Px^3*Qx^4*Rx^2*Ry - 18*Px^2*Qx^5*Rx^2*Ry - 6*Qx^7*Rx^2*Ry + 20*Px^3*Qx^3*Rx^3*Ry - 15*Px^2*Qx^4*Rx^3*Ry + 10*Qx^6*Rx^3*Ry + 30*Px^2*Qx^3*Rx^4*Ry + 6*Qx^5*Rx^4*Ry - 6*Px^3*Qx*Rx^5*Ry - 9*Px^2*Qx^2*Rx^5*Ry - 12*Qx^4*Rx^5*Ry + 2*Px^3*Rx^6*Ry - 6*Px^2*Qx*Rx^6*Ry - 2*Qx^3*Rx^6*Ry + 3*Px^2*Rx^7*Ry + 6*Qx^2*Rx^7*Ry - Rx^9*Ry + Py^3*Qx^6 - 3*Py^2*Qx^6*Qy - 6*Px*Py*Qx^5*Qy^2 - 3*Py*Qx^6*Qy^2 - 2*Px^3*Qx^3*Qy^3 - 6*Px^2*Qx^4*Qy^3 + 3*Qx^6*Qy^3 - 6*Py^3*Qx^5*Rx + 9*Py^2*Qx^5*Qy*Rx + 18*Px*Py*Qx^4*Qy^2*Rx + 12*Py*Qx^5*Qy^2*Rx + 6*Px^3*Qx^2*Qy^3*Rx + 9*Px^2*Qx^3*Qy^3*Rx + 15*Py^3*Qx^4*Rx^2 - 12*Px*Py*Qx^3*Qy^2*Rx^2 - 12*Py*Qx^4*Qy^2*Rx^2 - 6*Px^3*Qx*Qy^3*Rx^2 + 9*Px^2*Qx^2*Qy^3*Rx^2 - 12*Qx^4*Qy^3*Rx^2 - 20*Py^3*Qx^3*Rx^3 - 30*Py^2*Qx^3*Qy*Rx^3 - 12*Px*Py*Qx^2*Qy^2*Rx^3 - 12*Py*Qx^3*Qy^2*Rx^3 + 2*Px^3*Qy^3*Rx^3 - 21*Px^2*Qx*Qy^3*Rx^3 + 5*Qx^3*Qy^3*Rx^3 + 15*Py^3*Qx^2*Rx^4 + 45*Py^2*Qx^2*Qy*Rx^4 + 18*Px*Py*Qx*Qy^2*Rx^4 + 33*Py*Qx^2*Qy^2*Rx^4 + 9*Px^2*Qy^3*Rx^4 + 12*Qx^2*Qy^3*Rx^4 - 6*Py^3*Qx*Rx^5 - 27*Py^2*Qx*Qy*Rx^5 - 6*Px*Py*Qy^2*Rx^5 - 24*Py*Qx*Qy^2*Rx^5 - 9*Qx*Qy^3*Rx^5 + Py^3*Rx^6 + 6*Py^2*Qy*Rx^6 + 6*Py*Qy^2*Rx^6 + Qy^3*Rx^6 + 6*Py^2*Qx^6*Ry + 12*Px*Py*Qx^5*Qy*Ry + 6*Px^3*Qx^3*Qy^2*Ry + 21*Px^2*Qx^4*Qy^2*Ry - 9*Qx^6*Qy^2*Ry - 27*Py^2*Qx^5*Rx*Ry - 36*Px*Py*Qx^4*Qy*Rx*Ry - 6*Py*Qx^5*Qy*Rx*Ry - 18*Px^3*Qx^2*Qy^2*Rx*Ry - 39*Px^2*Qx^3*Qy^2*Rx*Ry + 6*Qx^5*Qy^2*Rx*Ry + 45*Py^2*Qx^4*Rx^2*Ry + 24*Px*Py*Qx^3*Qy*Rx^2*Ry + 24*Py*Qx^4*Qy*Rx^2*Ry + 18*Px^3*Qx*Qy^2*Rx^2*Ry - 9*Px^2*Qx^2*Qy^2*Rx^2*Ry + 21*Qx^4*Qy^2*Rx^2*Ry - 30*Py^2*Qx^3*Rx^3*Ry + 24*Px*Py*Qx^2*Qy*Rx^3*Ry - 36*Py*Qx^3*Qy*Rx^3*Ry - 6*Px^3*Qy^2*Rx^3*Ry + 51*Px^2*Qx*Qy^2*Rx^3*Ry - 15*Qx^3*Qy^2*Rx^3*Ry - 36*Px*Py*Qx*Qy*Rx^4*Ry + 24*Py*Qx^2*Qy*Rx^4*Ry - 24*Px^2*Qy^2*Rx^4*Ry - 6*Qx^2*Qy^2*Rx^4*Ry + 9*Py^2*Qx*Rx^5*Ry + 12*Px*Py*Qy*Rx^5*Ry - 6*Py*Qx*Qy*Rx^5*Ry - 3*Qx*Qy^2*Rx^5*Ry - 3*Py^2*Rx^6*Ry + 6*Qy^2*Rx^6*Ry - 6*Px*Py*Qx^5*Ry^2 + 6*Py*Qx^6*Ry^2 - 6*Px^3*Qx^3*Qy*Ry^2 - 24*Px^2*Qx^4*Qy*Ry^2 + 6*Qx^6*Qy*Ry^2 + 18*Px*Py*Qx^4*Rx*Ry^2 - 24*Py*Qx^5*Rx*Ry^2 + 18*Px^3*Qx^2*Qy*Rx*Ry^2 + 51*Px^2*Qx^3*Qy*Rx*Ry^2 - 3*Qx^5*Qy*Rx*Ry^2 - 12*Px*Py*Qx^3*Rx^2*Ry^2 + 33*Py*Qx^4*Rx^2*Ry^2 - 18*Px^3*Qx*Qy*Rx^2*Ry^2 - 9*Px^2*Qx^2*Qy*Rx^2*Ry^2 - 6*Qx^4*Qy*Rx^2*Ry^2 - 12*Px*Py*Qx^2*Rx^3*Ry^2 - 12*Py*Qx^3*Rx^3*Ry^2 + 6*Px^3*Qy*Rx^3*Ry^2 - 39*Px^2*Qx*Qy*Rx^3*Ry^2 - 15*Qx^3*Qy*Rx^3*Ry^2 + 18*Px*Py*Qx*Rx^4*Ry^2 - 12*Py*Qx^2*Rx^4*Ry^2 + 21*Px^2*Qy*Rx^4*Ry^2 + 21*Qx^2*Qy*Rx^4*Ry^2 - 6*Px*Py*Rx^5*Ry^2 + 12*Py*Qx*Rx^5*Ry^2 + 6*Qx*Qy*Rx^5*Ry^2 - 3*Py*Rx^6*Ry^2 - 9*Qy*Rx^6*Ry^2 + 2*Px^3*Qx^3*Ry^3 + 9*Px^2*Qx^4*Ry^3 + Qx^6*Ry^3 - 6*Px^3*Qx^2*Rx*Ry^3 - 21*Px^2*Qx^3*Rx*Ry^3 - 9*Qx^5*Rx*Ry^3 + 6*Px^3*Qx*Rx^2*Ry^3 + 9*Px^2*Qx^2*Rx^2*Ry^3 + 12*Qx^4*Rx^2*Ry^3 - 2*Px^3*Rx^3*Ry^3 + 9*Px^2*Qx*Rx^3*Ry^3 + 5*Qx^3*Rx^3*Ry^3 - 6*Px^2*Rx^4*Ry^3 - 12*Qx^2*Rx^4*Ry^3 + 3*Rx^6*Ry^3 + 3*Py^2*Qx^3*Qy^3 + 3*Px*Py*Qx^2*Qy^4 + 3*Px^2*Qx*Qy^5 - 3*Qx^3*Qy^5 - 9*Py^2*Qx^2*Qy^3*Rx - 6*Px*Py*Qx*Qy^4*Rx - 6*Py*Qx^2*Qy^4*Rx - 3*Px^2*Qy^5*Rx + 9*Py^2*Qx*Qy^3*Rx^2 + 3*Px*Py*Qy^4*Rx^2 + 12*Py*Qx*Qy^4*Rx^2 + 6*Qx*Qy^5*Rx^2 - 3*Py^2*Qy^3*Rx^3 - 6*Py*Qy^4*Rx^3 - 3*Qy^5*Rx^3 - 9*Py^2*Qx^3*Qy^2*Ry - 12*Px*Py*Qx^2*Qy^3*Ry + 6*Py*Qx^3*Qy^3*Ry - 15*Px^2*Qx*Qy^4*Ry + 12*Qx^3*Qy^4*Ry + 27*Py^2*Qx^2*Qy^2*Rx*Ry + 24*Px*Py*Qx*Qy^3*Rx*Ry + 6*Py*Qx^2*Qy^3*Rx*Ry + 15*Px^2*Qy^4*Rx*Ry - 3*Qx^2*Qy^4*Rx*Ry - 27*Py^2*Qx*Qy^2*Rx^2*Ry - 12*Px*Py*Qy^3*Rx^2*Ry - 30*Py*Qx*Qy^3*Rx^2*Ry - 15*Qx*Qy^4*Rx^2*Ry + 9*Py^2*Qy^2*Rx^3*Ry + 18*Py*Qy^3*Rx^3*Ry + 6*Qy^4*Rx^3*Ry + 9*Py^2*Qx^3*Qy*Ry^2 + 18*Px*Py*Qx^2*Qy^2*Ry^2 - 18*Py*Qx^3*Qy^2*Ry^2 + 30*Px^2*Qx*Qy^3*Ry^2 - 15*Qx^3*Qy^3*Ry^2 - 27*Py^2*Qx^2*Qy*Rx*Ry^2 - 36*Px*Py*Qx*Qy^2*Rx*Ry^2 + 18*Py*Qx^2*Qy^2*Rx*Ry^2 - 30*Px^2*Qy^3*Rx*Ry^2 + 3*Qx^2*Qy^3*Rx*Ry^2 + 27*Py^2*Qx*Qy*Rx^2*Ry^2 + 18*Px*Py*Qy^2*Rx^2*Ry^2 + 18*Py*Qx*Qy^2*Rx^2*Ry^2 + 9*Qx*Qy^3*Rx^2*Ry^2 - 9*Py^2*Qy*Rx^3*Ry^2 - 18*Py*Qy^2*Rx^3*Ry^2 + 3*Qy^3*Rx^3*Ry^2 - 3*Py^2*Qx^3*Ry^3 - 12*Px*Py*Qx^2*Qy*Ry^3 + 18*Py*Qx^3*Qy*Ry^3 - 30*Px^2*Qx*Qy^2*Ry^3 + 3*Qx^3*Qy^2*Ry^3 + 9*Py^2*Qx^2*Rx*Ry^3 + 24*Px*Py*Qx*Qy*Rx*Ry^3 - 30*Py*Qx^2*Qy*Rx*Ry^3 + 30*Px^2*Qy^2*Rx*Ry^3 + 9*Qx^2*Qy^2*Rx*Ry^3 - 9*Py^2*Qx*Rx^2*Ry^3 - 12*Px*Py*Qy*Rx^2*Ry^3 + 6*Py*Qx*Qy*Rx^2*Ry^3 + 3*Qx*Qy^2*Rx^2*Ry^3 + 3*Py^2*Rx^3*Ry^3 + 6*Py*Qy*Rx^3*Ry^3 - 15*Qy^2*Rx^3*Ry^3 + 3*Px*Py*Qx^2*Ry^4 - 6*Py*Qx^3*Ry^4 + 15*Px^2*Qx*Qy*Ry^4 + 6*Qx^3*Qy*Ry^4 - 6*Px*Py*Qx*Rx*Ry^4 + 12*Py*Qx^2*Rx*Ry^4 - 15*Px^2*Qy*Rx*Ry^4 - 15*Qx^2*Qy*Rx*Ry^4 + 3*Px*Py*Rx^2*Ry^4 - 6*Py*Qx*Rx^2*Ry^4 - 3*Qx*Qy*Rx^2*Ry^4 + 12*Qy*Rx^3*Ry^4 - 3*Px^2*Qx*Ry^5 - 3*Qx^3*Ry^5 + 3*Px^2*Rx*Ry^5 + 6*Qx^2*Rx*Ry^5 - 3*Rx^3*Ry^5 + Py*Qy^6 + Qy^7 - 6*Py*Qy^5*Ry - 5*Qy^6*Ry + 15*Py*Qy^4*Ry^2 + 9*Qy^5*Ry^2 - 20*Py*Qy^3*Ry^3 - 5*Qy^4*Ry^3 + 15*Py*Qy^2*Ry^4 - 5*Qy^3*Ry^4 - 6*Py*Qy*Ry^5 + 9*Qy^2*Ry^5 + Py*Ry^6 - 5*Qy*Ry^6 + Ry^7)/(-Px^3*Qx^6 - 3*Px^2*Qx^7 - 3*Px*Qx^8 - Qx^9 + 6*Px^3*Qx^5*Rx + 15*Px^2*Qx^6*Rx + 12*Px*Qx^7*Rx + 3*Qx^8*Rx - 15*Px^3*Qx^4*Rx^2 - 27*Px^2*Qx^5*Rx^2 - 12*Px*Qx^6*Rx^2 + 20*Px^3*Qx^3*Rx^3 + 15*Px^2*Qx^4*Rx^3 - 12*Px*Qx^5*Rx^3 - 8*Qx^6*Rx^3 - 15*Px^3*Qx^2*Rx^4 + 15*Px^2*Qx^3*Rx^4 + 30*Px*Qx^4*Rx^4 + 6*Qx^5*Rx^4 + 6*Px^3*Qx*Rx^5 - 27*Px^2*Qx^2*Rx^5 - 12*Px*Qx^3*Rx^5 + 6*Qx^4*Rx^5 - Px^3*Rx^6 + 15*Px^2*Qx*Rx^6 - 12*Px*Qx^2*Rx^6 - 8*Qx^3*Rx^6 - 3*Px^2*Rx^7 + 12*Px*Qx*Rx^7 - 3*Px*Rx^8 + 3*Qx*Rx^8 - Rx^9 + 3*Px^2*Qx^4*Qy^2 + 6*Px*Qx^5*Qy^2 + 3*Qx^6*Qy^2 - 12*Px^2*Qx^3*Qy^2*Rx - 18*Px*Qx^4*Qy^2*Rx - 6*Qx^5*Qy^2*Rx + 18*Px^2*Qx^2*Qy^2*Rx^2 + 12*Px*Qx^3*Qy^2*Rx^2 - 3*Qx^4*Qy^2*Rx^2 - 12*Px^2*Qx*Qy^2*Rx^3 + 12*Px*Qx^2*Qy^2*Rx^3 + 12*Qx^3*Qy^2*Rx^3 + 3*Px^2*Qy^2*Rx^4 - 18*Px*Qx*Qy^2*Rx^4 - 3*Qx^2*Qy^2*Rx^4 + 6*Px*Qy^2*Rx^5 - 6*Qx*Qy^2*Rx^5 + 3*Qy^2*Rx^6 - 6*Px^2*Qx^4*Qy*Ry - 12*Px*Qx^5*Qy*Ry - 6*Qx^6*Qy*Ry + 24*Px^2*Qx^3*Qy*Rx*Ry + 36*Px*Qx^4*Qy*Rx*Ry + 12*Qx^5*Qy*Rx*Ry - 36*Px^2*Qx^2*Qy*Rx^2*Ry - 24*Px*Qx^3*Qy*Rx^2*Ry + 6*Qx^4*Qy*Rx^2*Ry + 24*Px^2*Qx*Qy*Rx^3*Ry - 24*Px*Qx^2*Qy*Rx^3*Ry - 24*Qx^3*Qy*Rx^3*Ry - 6*Px^2*Qy*Rx^4*Ry + 36*Px*Qx*Qy*Rx^4*Ry + 6*Qx^2*Qy*Rx^4*Ry - 12*Px*Qy*Rx^5*Ry + 12*Qx*Qy*Rx^5*Ry - 6*Qy*Rx^6*Ry + 3*Px^2*Qx^4*Ry^2 + 6*Px*Qx^5*Ry^2 + 3*Qx^6*Ry^2 - 12*Px^2*Qx^3*Rx*Ry^2 - 18*Px*Qx^4*Rx*Ry^2 - 6*Qx^5*Rx*Ry^2 + 18*Px^2*Qx^2*Rx^2*Ry^2 + 12*Px*Qx^3*Rx^2*Ry^2 - 3*Qx^4*Rx^2*Ry^2 - 12*Px^2*Qx*Rx^3*Ry^2 + 12*Px*Qx^2*Rx^3*Ry^2 + 12*Qx^3*Rx^3*Ry^2 + 3*Px^2*Rx^4*Ry^2 - 18*Px*Qx*Rx^4*Ry^2 - 3*Qx^2*Rx^4*Ry^2 + 6*Px*Rx^5*Ry^2 - 6*Qx*Rx^5*Ry^2 + 3*Rx^6*Ry^2 - 3*Px*Qx^2*Qy^4 - 3*Qx^3*Qy^4 + 6*Px*Qx*Qy^4*Rx + 3*Qx^2*Qy^4*Rx - 3*Px*Qy^4*Rx^2 + 3*Qx*Qy^4*Rx^2 - 3*Qy^4*Rx^3 + 12*Px*Qx^2*Qy^3*Ry + 12*Qx^3*Qy^3*Ry - 24*Px*Qx*Qy^3*Rx*Ry - 12*Qx^2*Qy^3*Rx*Ry + 12*Px*Qy^3*Rx^2*Ry - 12*Qx*Qy^3*Rx^2*Ry + 12*Qy^3*Rx^3*Ry - 18*Px*Qx^2*Qy^2*Ry^2 - 18*Qx^3*Qy^2*Ry^2 + 36*Px*Qx*Qy^2*Rx*Ry^2 + 18*Qx^2*Qy^2*Rx*Ry^2 - 18*Px*Qy^2*Rx^2*Ry^2 + 18*Qx*Qy^2*Rx^2*Ry^2 - 18*Qy^2*Rx^3*Ry^2 + 12*Px*Qx^2*Qy*Ry^3 + 12*Qx^3*Qy*Ry^3 - 24*Px*Qx*Qy*Rx*Ry^3 - 12*Qx^2*Qy*Rx*Ry^3 + 12*Px*Qy*Rx^2*Ry^3 - 12*Qx*Qy*Rx^2*Ry^3 + 12*Qy*Rx^3*Ry^3 - 3*Px*Qx^2*Ry^4 - 3*Qx^3*Ry^4 + 6*Px*Qx*Rx*Ry^4 + 3*Qx^2*Rx*Ry^4 - 3*Px*Rx^2*Ry^4 + 3*Qx*Rx^2*Ry^4 - 3*Rx^3*Ry^4 + Qy^6 - 6*Qy^5*Ry + 15*Qy^4*Ry^2 - 20*Qy^3*Ry^3 + 15*Qy^2*Ry^4 - 6*Qy*Ry^5 + Ry^6), 1)