17
s u1 t1 t2 t3 v1 u2 t4 v2 u3 v3 x1 x2 x3 y4 y5 y6
# Pappus theorem
# A(x1,0), B(x2,0) and C(x3,0) are on one line.
# D(0,y4), E(0,y5) and F(0,y6) are on the other line.
# we put the negation of the theorem as well.

s u1 v2 - s u1 v3 + t1^3

t1^3 - s u2 v3 - s v1 u3 + s v2 u3 + s v1 u2 - 1

t2^2 - x1 v1 + x1 y5

u1 y5 + t2^2

x2 v1 - x2 y4 - t3^2

u1 y4 + t3^2

x1 v2 - x1 y6 -t4^2

u2 y6 + t4^2

x3 v2 + u2 y4 - x3 y4

x2 v3 + u3 y6 - x2 y6

x3 v3 + u3 y5 - x3 y5









