fof(goal, conjecture,(![L1,L2,L3,A,B,C]:((line(L1)&line(L2)&line(L3)&point(A)&point(B)&point(C)&L1!=L2&L2!=L3&L3!=L1&int_l_l(L1,L2)&int_l_l(L2,L3)&int_l_l(L3,L1)&inc_po_l(A,L1)&inc_po_l(A,L2)&ninc_po_l(A,L3)&ninc_po_l(B,L1)&inc_po_l(B,L2)&inc_po_l(B,L3)&inc_po_l(C,L1)&ninc_po_l(C,L2)&inc_po_l(C,L3)&A!=B&B!=C&C!=A&ncol(A,B,C))=>(?[P]:(plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)))))).
