11
x1 x2 x3 x4 x5 x6 x7 u1 u2 u3 u4
# Butterfly theorem
# Described in "A collection of Geometry Theorems Proved Mechanically" by Shang-Ching Chou
# (Institute for Computer Science, University of Texas at Austin, Technical Report 50)

-x1^2 + 2 u1 x1 - u4^2 + u3^2 + u2^2 - 2 u1 u2

-x3^2 + 2 u1 x3 - x2^2 + u3^2 + u2^2 - 2 u1 u2

- u3 x3 + u2 x2

- x2^2 + 2 u1 x5 - x4^2 + u3^2 + u2^2 - 2 u1 u2

- u4 x5 + x1 x4

- x5 x6 + u2 x6 + u3 x5 - u2 x4

- x3 x7 + x1 x7 + u4 x3 - x1 x2




