# A theorem in solid geometry from D. Wang's Ph.D thesis
Solid := Theorem(
     [2*u1*x7-u1*(u2+u4),
      2*(u2-u1)*x7+2*u3*x8-u4*(u2-u1)-u3*u5,
      2*(u4-u2)*x7+2*(u5-u3)*x8+2*u6*x9-u1*(u4-u2),
      (2*u2-u1)*x11-2*u3*x10+u1*u3,
      (u2-2*u1)*x11-u3*x10+u1*u3,
      4*x12-3*x10-u4, 4*x13-3*x11-u5,
      4*x14-u6, 2*x15-u1,
      2*u2*x15+2*u3*x16-u2^2-u3^2,
      2*u4*x15+2*u5*x16+2*u6*x17-u4^2-u5^2-u6^2],
     {x13*x15+x7*x16+x8*x12-x7*x13-x8*x15-x12*x16,
      x9*x12+x14*x15+x7*x17-x7*x14-x9*x15-x12*x17},
     [u1, u2, u3, u4, u5, u6, x7, x8, x9, x10, x11, x12, 
      x13, x14, x15, x16, x17]);
