assume [A,B,C,L] : (point(A) & point(B) & line(L) & A != B & on(A,L) & on(B,L) & point(C) & cong(A,B,B,C) & cong(B,C,C,A))
infer (C!=A)
infer (C!=B)
infer (non(C,L))
