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)&A!=B&B!=C&C!=A&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))=>(?[P]:(plane(P)&inc_l_pl(L1,P)&inc_l_pl(L2,P)&inc_l_pl(L3,P))))).
