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