fof(ax_branch_inc_po_l,axiom,(![A,L]:((point(A)&line(L))=>(inc_po_l(A,L)|ninc_po_l(A,L))))).

fof(ax_branch_inc_po_pl,axiom,(![A,P]:((point(A)&plane(P))=>(inc_po_pl(A,P)|ninc_po_pl(A,P))))).

fof(ax_branch_bet,axiom,(![A,B,C]:((point(A)&point(B)&point(C))=>(bet(A,B,C)|nbet(A,B,C))))).

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

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

fof(ax_D1a,axiom,(![A,B,C,L]:((point(A)&point(B)&A!=B&point(C)&line(L)&inc_po_l(A,L)&inc_po_l(B,L)&ninc_po_l(C,L))=>(ncol(A,B,C))))).

fof(ax_D2a,axiom,(![A,B,C,L]:((point(A)&point(B)&A!=B&point(C)&line(L)&inc_po_l(A,L)&inc_po_l(B,L)&ncol(A,B,C))=>(ninc_po_l(C,L))))).

fof(ax_branch_col,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&A!=B&A!=C&B!=C)=>(col(A,B,C)|ncol(A,B,C))))).

fof(ax_sym_col1,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&col(A,B,C))=>(col(B,C,A))))).

fof(ax_sym_ncol1,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&ncol(A,B,C))=>(ncol(B,C,A))))).

fof(ax_sym_col2,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&col(A,B,C))=>(col(B,A,C))))).

fof(ax_sym_ncol2,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&ncol(A,B,C))=>(ncol(B,A,C))))).

fof(ax_sym_col,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&col(A,B,C))=>(col(A,C,B)&col(B,A,C)&col(B,C,A)&col(C,A,B)&col(C,B,A))))).

fof(ax_sym_ncol,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&ncol(A,B,C))=>(ncol(A,C,B)&ncol(B,A,C)&ncol(B,C,A)&ncol(C,A,B)&ncol(C,B,A))))).

fof(ax_D3,axiom,(![A,B,C,D,P]:((point(A)&point(B)&point(C)&point(D)&plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)&inc_po_pl(D,P))=>(cop(A,B,C,D))))).

fof(ax_D4,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&cop(A,B,C,D))=>(?[P]:(plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)&inc_po_pl(D,P)))))).

fof(ax_D3a,axiom,(![A,B,C,D,P]:((point(A)&point(B)&point(C)&ncol(A,B,C)&point(D)&plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)&ninc_po_pl(D,P))=>(ncop(A,B,C,D))))).

fof(ax_D4a,axiom,(![A,B,C,D,P]:((point(A)&point(B)&point(C)&ncol(A,B,C)&point(D)&plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)&ncop(A,B,C,D))=>(ninc_po_pl(D,P))))).

fof(ax_branch_cop,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&A!=B&A!=C&A!=D&B!=C&B!=D&C!=D)=>(cop(A,B,C,D)|ncop(A,B,C,D))))).

fof(ax_sym_cop1,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&cop(A,B,C,D))=>(cop(B,C,D,A))))).

fof(ax_sym_ncop1,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&ncop(A,B,C,D))=>(ncop(B,C,D,A))))).

fof(ax_sym_cop2,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&cop(A,B,C,D))=>(cop(B,A,C,D))))).

fof(ax_sym_ncop2,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&ncop(A,B,C,D))=>(ncop(B,A,C,D))))).

fof(ax_sym_cop,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&cop(A,B,C,D))=>(cop(A,B,D,C)&cop(A,C,B,D)&cop(A,C,D,B)&cop(A,D,B,C)&cop(A,D,C,B)&cop(B,A,C,D)&cop(B,A,D,C)&cop(B,C,A,D)&cop(B,C,D,A)&cop(B,D,A,C)&cop(B,D,C,A)&cop(C,A,B,D)&cop(C,A,D,B)&cop(C,B,A,D)&cop(C,B,D,A)&cop(C,D,A,B)&cop(C,D,B,A)&cop(D,A,B,C)&cop(D,A,C,B)&cop(D,B,A,C)&cop(D,B,C,A)&cop(D,C,A,B)&cop(D,C,B,A))))).

fof(ax_sym_ncop,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&ncop(A,B,C,D))=>(ncop(A,B,D,C)&ncop(A,C,B,D)&ncop(A,C,D,B)&ncop(A,D,B,C)&ncop(A,D,C,B)&ncop(B,A,C,D)&ncop(B,A,D,C)&ncop(B,C,A,D)&ncop(B,C,D,A)&ncop(B,D,A,C)&ncop(B,D,C,A)&ncop(C,A,B,D)&ncop(C,A,D,B)&ncop(C,B,A,D)&ncop(C,B,D,A)&ncop(C,D,A,B)&ncop(C,D,B,A)&ncop(D,A,B,C)&ncop(D,A,C,B)&ncop(D,B,A,C)&ncop(D,B,C,A)&ncop(D,C,A,B)&ncop(D,C,B,A))))).

fof(ax_D5,axiom,(![L1,L2,A]:((line(L1)&line(L2)&point(A)&L1!=L2&inc_po_l(A,L1)&inc_po_l(A,L2))=>(int_l_l(L1,L2))))).

fof(ax_D6,axiom,(![L1,L2]:((line(L1)&line(L2)&int_l_l(L1,L2))=>(?[A]:(point(A)&L1!=L2&inc_po_l(A,L1)&inc_po_l(A,L2)))))).

fof(ax_D7,axiom,(![P1,P2,A]:((plane(P1)&plane(P2)&point(A)&P1!=P2&inc_po_pl(A,P1)&inc_po_pl(A,P2))=>(int_pl_pl(P1,P2))))).

fof(ax_D8,axiom,(![P1,P2]:((plane(P1)&plane(P2)&int_pl_pl(P1,P2))=>(?[A]:(point(A)&P1!=P2&inc_po_pl(A,P1)&inc_po_pl(A,P2)))))).

fof(ax_D9,axiom,(![L,P,A]:((line(L)&plane(P)&point(A)&ninc_l_pl(L,P)&inc_po_l(A,L)&inc_po_pl(A,P))=>(int_l_pl(L,P))))).

fof(ax_D10,axiom,(![L,P]:((line(L)&plane(P)&int_l_pl(L,P))=>(?[A]:(point(A)&inc_po_l(A,L)&inc_po_pl(A,P)&ninc_l_pl(L,P)))))).

fof(ax_D5a,axiom,(![L1,L2,A]:((line(L1)&line(L2)&point(A)&L1!=L2&nint_l_l(L1,L2)&inc_po_l(A,L1))=>(ninc_po_l(A,L2))))).

fof(ax_D7a,axiom,(![P1,P2,A]:((plane(P1)&plane(P2)&point(A)&P1!=P2&inc_po_pl(A,P1)&nint_pl_pl(P1,P2))=>(ninc_po_pl(A,P2))))).

fof(ax_D9a,axiom,(![L,P,A]:((line(L)&plane(P)&point(A)&ninc_l_pl(L,P)&nint_l_pl(L,P)&inc_po_l(A,L))=>(ninc_po_pl(A,P))))).

fof(ax_D9b,axiom,(![L,P,A]:((line(L)&plane(P)&point(A)&ninc_l_pl(L,P)&nint_l_pl(L,P)&inc_po_pl(A,P))=>(ninc_po_l(A,L))))).

fof(ax_branch_int_l_l,axiom,(![L1,L2]:((line(L1)&line(L2)&L1!=L2)=>(int_l_l(L1,L2)|nint_l_l(L1,L2))))).

fof(ax_branch_int_pl_pl,axiom,(![P1,P2]:((plane(P1)&plane(P2)&P1!=P2)=>(int_pl_pl(P1,P2)|nint_pl_pl(P1,P2))))).

fof(ax_branch_int_l_pl,axiom,(![L,P]:((line(L)&plane(P))=>(int_l_pl(L,P)|nint_l_pl(L,P))))).

fof(ax_sym_int_l_l,axiom,(![L1,L2]:((line(L1)&line(L2)&int_l_l(L1,L2))=>(int_l_l(L2,L1))))).

fof(ax_sym_nint_l_l,axiom,(![L1,L2]:((line(L1)&line(L2)&nint_l_l(L1,L2))=>(nint_l_l(L2,L1))))).

fof(ax_sym_int_pl_pl,axiom,(![P1,P2]:((plane(P1)&plane(P2)&int_pl_pl(P1,P2))=>(int_pl_pl(P2,P1))))).

fof(ax_sym_nint_pl_pl,axiom,(![P1,P2]:((plane(P1)&plane(P2)&nint_pl_pl(P1,P2))=>(nint_pl_pl(P2,P1))))).

fof(ax_D11,axiom,(![A,L,P]:((point(A)&line(L)&plane(P)&inc_l_pl(L,P)&inc_po_l(A,L))=>(inc_po_pl(A,P))))).

fof(ax_D11a,axiom,(![L,P]:((line(L)&plane(P)&ninc_l_pl(L,P))=>(?[A]:(point(A)&inc_po_l(A,L)&ninc_po_pl(A,P)))))).

fof(ax_D11b,axiom,(![A,L,P]:((point(A)&line(L)&plane(P)&inc_po_l(A,L)&ninc_po_pl(A,P))=>(ninc_l_pl(L,P))))).

fof(ax_branch_inc_l_pl,axiom,(![L,P]:((line(L)&plane(P))=>(inc_l_pl(L,P)|ninc_l_pl(L,P))))).

fof(ax_false_bet,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&bet(A,B,C)&nbet(A,B,C))=>$false))).

fof(ax_false_inc_po_l,axiom,(![A,L]:((point(A)&line(L)&inc_po_l(A,L)&ninc_po_l(A,L))=>$false))).

fof(ax_false_inc_po_pl,axiom,(![A,P]:((point(A)&plane(P)&inc_po_pl(A,P)&ninc_po_pl(A,P))=>$false))).

fof(ax_false_inc_l_pl,axiom,(![L,P]:((line(L)&plane(P)&inc_l_pl(L,P)&ninc_l_pl(L,P))=>$false))).

fof(ax_false_int_l_l,axiom,(![L1,L2]:((line(L1)&line(L2)&int_l_l(L1,L2)&nint_l_l(L1,L2))=>$false))).

fof(ax_false_int_l_pl,axiom,(![L,P]:((line(L)&plane(P)&int_l_pl(L,P)&nint_l_pl(L,P))=>$false))).

fof(ax_false_int_pl_pl,axiom,(![P1,P2]:((plane(P1)&plane(P2)&int_pl_pl(P1,P2)&nint_pl_pl(P1,P2))=>$false))).

fof(ax_false_col,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&col(A,B,C)&ncol(A,B,C))=>$false))).

fof(ax_false_cop,axiom,(![A,B,C,D]:((point(A)&point(B)&point(C)&point(D)&cop(A,B,C,D)&ncop(A,B,C,D))=>$false))).

fof(ax_I1,axiom,(![A,B]:((point(A)&point(B)&A!=B)=>(?[L]:(line(L)&inc_po_l(A,L)&inc_po_l(B,L)))))).

fof(ax_I2,axiom,(![A,B,L1,L2]:((point(A)&point(B)&line(L1)&line(L2)&A!=B&inc_po_l(A,L1)&inc_po_l(B,L1)&inc_po_l(A,L2)&inc_po_l(B,L2))=>(L1=L2)))).

fof(ax_I3a,axiom,(![L]:((line(L))=>(?[A,B]:(point(A)&point(B)&A!=B&inc_po_l(A,L)&inc_po_l(B,L)))))).

fof(ax_I3b,axiom,(?[A,B,C]:(point(A)&point(B)&point(C)&ncol(A,B,C)))).

fof(ax_I4a,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&ncol(A,B,C))=>(?[P]:(plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)))))).

fof(ax_I4b,axiom,(![P]:((plane(P))=>(?[A]:(point(A)&inc_po_pl(A,P)))))).

fof(ax_I5,axiom,(![A,B,C,P1,P2]:((point(A)&point(B)&point(C)&plane(P1)&plane(P2)&ncol(A,B,C)&inc_po_pl(A,P1)&inc_po_pl(B,P1)&inc_po_pl(C,P1)&inc_po_pl(A,P2)&inc_po_pl(B,P2)&inc_po_pl(C,P2))=>(P1=P2)))).

fof(ax_I6,axiom,(![A,B,L,P]:((point(A)&point(B)&line(L)&plane(P)&A!=B&inc_po_l(A,L)&inc_po_l(B,L)&inc_po_pl(A,P)&inc_po_pl(B,P))=>(inc_l_pl(L,P))))).

fof(ax_I7,axiom,(![P1,P2,A]:((plane(P1)&plane(P2)&point(A)&P1!=P2&inc_po_pl(A,P1)&inc_po_pl(A,P2))=>(?[B]:(point(B)&A!=B&inc_po_pl(B,P1)&inc_po_pl(B,P2)))))).

fof(ax_I8,axiom,(?[A,B,C,D]:(point(A)&point(B)&point(C)&point(D)&ncop(A,B,C,D)))).

fof(ax_II1,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&bet(A,B,C))=>(A!=B&A!=C&B!=C&col(A,B,C)&bet(C,B,A))))).

fof(ax_II2,axiom,(![A,B]:((point(A)&point(B)&A!=B)=>(?[C]:(point(C)&bet(A,B,C)))))).

fof(ax_II3,axiom,(![A,B,C]:((point(A)&point(B)&point(C)&A!=B&A!=C&B!=C&bet(A,B,C))=>(nbet(B,C,A)&nbet(C,A,B))))).

fof(ax_cut_1,axiom,(![L,A,B,X]:((point(A)&point(B)&line(L)&point(X)&ninc_po_l(A,L)&ninc_po_l(B,L)&inc_po_l(X,L)&bet(A,X,B))=>(cut(L,A,B))))).

fof(ax_cut_2,axiom,(![L,A,B]:((point(A)&point(B)&line(L)&cut(L,A,B))=>(?[X]:(point(X)&ninc_po_l(A,L)&ninc_po_l(B,L)&inc_po_l(X,L)&bet(A,X,B)))))).

fof(ax_pash_1,axiom,(![A,B,C,L,P]:((point(A)&point(B)&point(C)&line(L)&plane(P)&ncol(A,B,C)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)&inc_l_pl(L,P)&ninc_po_l(A,L)&ninc_po_l(B,L)&ninc_po_l(C,L)&cut(L,B,C))=>pash(A,B,C,L,P)))).

fof(ax_pash_2,axiom,(![A,B,C,L,P]:((point(A)&point(B)&point(C)&line(L)&plane(P)&pash(A,B,C,L,P))=>(ncol(A,B,C)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P)&inc_l_pl(L,P)&ninc_po_l(A,L)&ninc_po_l(B,L)&ninc_po_l(C,L)&cut(L,B,C))))).

fof(ax_II4,axiom,(![A,B,C,L,P]:((point(A)&point(B)&point(C)&line(L)&plane(P)&pash(A,B,C,L,P))=>(cut(L,C,A)|cut(L,A,B))))).

fof(ax_false_cut,axiom,(![L,A,B]:((point(A)&point(B)&line(L)&cut(L,A,B)&ncut(L,A,B))=>$false))).

fof(ax_branch_cut,axiom,(![L,A,B]:((point(A)&point(B)&A!=B&line(L))=>(cut(L,A,B)|ncut(L,A,B))))).

fof(ax_false_pash,axiom,(![A,B,C,L,P]:((point(A)&point(B)&point(C)&line(L)&plane(P)&pash(A,B,C,L,P)&npash(A,B,C,L,P))=>$false))).

fof(ax_branch_pash,axiom,(![A,B,C,L,P]:((point(A)&point(B)&point(C)&A!=B&A!=C&B!=C&line(L)&plane(P))=>(pash(A,B,C,L,P)|npash(A,B,C,L,P))))).

