fof(goal, conjecture,(![L,A,B,C]:((line(L)&point(A)&point(B)&point(C)&B!=C&inc_po_l(B,L)&inc_po_l(C,L)&col(A,B,C))=>(inc_po_l(A,L))))).
