assume [A,B,C] : (point(A) & point(B) & A!=B & point(C) & A=B)
construct [L] : (line(L) & on(A,L) & on(B,L))
%infer ($false)
