assume [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))
goal (construct [P] : (plane(P) & inc_l_pl(L1,P) & inc_l_pl(L2,P) & inc_l_pl(L3,P)))

infer (A != B & B != C & C != A)

infer (col(A,B,C) | ncol(A,B,C))

      case (col(A,B,C))
      construct [L] : (line(L) & inc_po_l(A,L) & inc_po_l(B,L) & inc_po_l(C,L))
      infer (L = L1 & L = L2 & L = L3)
      lookup contradiction      

      case (ncol(A,B,C))
      construct [P] : (plane(P) & inc_po_pl(A,P) & inc_po_pl(B,P) & inc_po_pl(C,P))
      infer (inc_l_pl(L1,P) & inc_l_pl(L2,P) & inc_l_pl(L3,P))
      lookup goal
