assume [A,B,C] : (point(A) & point(B) & point(C) & ncol(A,B,C))
goal (A != B & B != C & C != A)

infer (A = B | A != B)

case (A = B)
infer (col(A,B,C))
lookup contradiction

case (A != B)
infer (B!=C & C!=A)
lookup goal

