fof(ax_1,axiom,(![A,B]:((point(A) & point(B) & ) => (cong(A,B,B,A))))).

fof(ax_2,axiom,(![A,B,P,Q,R,S]:((point(A) & point(B) & point(P) & point(Q) & point(R) & point(S) & cong(A,B,P,Q)&cong(A,B,R,S))=>cong(P,Q,R,S)))).

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

fof(ax_4,axiom,(![A,B,C,Q]:((point(A) & point(B) & point(C) & point(Q) & ) => (?[X]:(bet(Q,A,X)&cong(A,X,B,C)))))).

fof(ax_5,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & A!=B&bet(A,B,C)&bet(A1,B1,C1)&cong(A,B,A1,B1)&cong(B,C,B1,C1)&cong(A,D,A1,D1)&cong(B,D,B1,D1))=>cong(C,D,C1,D1)))).

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

fof(ax_7,axiom,(![A,B,C,P,Q]:((point(A) & point(B) & point(C) & point(P) & point(Q) & bet(A,P,C)&bet(B,Q,C))=>(?[X]:(bet(P,X,B)&bet(Q,X,A)))))).

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

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_branch_cong,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & ) => (cong(A,B,C,D)|ncong(A,B,C,D))))).

fof(ax_false_cong,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)&ncong(A,B,C,D))=>$false))).

fof(ax_8,axiom,(?[A,B,C]:(() => (nbet(A,B,C)&nbet(B,C,A)&nbet(C,A,B))))).

fof(ax_9,axiom,(![P,Q,A,B,C]:((point(P) & point(Q) & point(A) & point(B) & point(C) & P!=Q&cong(A,P,A,Q)&cong(B,P,B,Q)&cong(C,P,C,Q))=>(bet(A,B,C)|bet(B,C,A)|bet(C,A,B))))).

fof(ax_10,axiom,(![A,B,C,D,T]:((point(A) & point(B) & point(C) & point(D) & point(T) & bet(A,D,T)&bet(B,D,C)&A!=D)=>(?[X,Y]:(bet(A,B,X)&bet(A,C,Y)&bet(X,T,Y)))))).

fof(th_2_1,axiom,(![A,B]:((point(A) & point(B) & ) => (cong(A,B,A,B))))).

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

fof(th_2_3,axiom,(![A,B,C,D,E,F]:((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))).

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

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

fof(th_2_8,axiom,(![A,B]:((point(A) & point(B) & ) => (cong(A,A,B,B))))).

fof(ax_2_10_1,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & afs(A,B,C,D,A1,B1,C1,D1))=>(bet(A,B,C)&bet(A1,B1,C1)&cong(A,B,A1,B1)&cong(B,C,B1,C1)&cong(A,D,A1,D1)&cong(B,D,B1,D1))))).

fof(ax_2_10_2,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & bet(A,B,C)&bet(A1,B1,C1)&cong(A,B,A1,B1)&cong(B,C,B1,C1)&cong(A,D,A1,D1)&cong(B,D,B1,D1))=>afs(A,B,C,D,A1,B1,C1,D1)))).

fof(ax_branch_afs,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & ) =>(afs(A,B,C,D,A1,B1,C1,D1)|nafs(A,B,C,D,A1,B1,C1,D1))))).

fof(ax_false_afs,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & afs(A,B,C,D,A1,B1,C1,D1)&nafs(A,B,C,D,A1,B1,C1,D1))=>$false))).

fof(th_2_11,axiom,(![A,B,C,A1,B1,C1]:((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(C1) & bet(A,B,C)&bet(A1,B1,C1)&cong(A,B,A1,B1)&cong(B,C,B1,C1))=>cong(A,C,A1,C1)))).

fof(th_2_12,axiom,(![A,B,C,Q,X,Y]:((point(A) & point(B) & point(C) & point(Q) & point(X) & point(Y) & Q!=A&bet(Q,A,X)&cong(A,X,B,C)&bet(Q,A,Y)&cong(A,Y,B,C))=>(X=Y)))).

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

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

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

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

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

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

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

fof(ax_3_8_1,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & bet4(A,B,C,D))=>(bet(A,B,C)&bet(A,B,D)&bet(A,C,D)&bet(B,C,D))))).

fof(ax_3_8_2,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & bet(A,B,C)&bet(A,B,D)&bet(A,C,D)&bet(B,C,D))=>bet4(A,B,C,D)))).

fof(ax_branch_bet4,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & ) => (bet4(A,B,C,D)|nbet4(A,B,C,D))))).

fof(ax_false_bet4,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & bet4(A,B,C,D)&nbet4(A,B,C,D))=>$false))).

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

fof(th_3_10_1,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & bet4(A,B,C,D))=>(bet(A,B,C))))).

fof(th_3_10_2,axiom,(![A,B,C,D]:((point(A) & point(B) & point(C) & point(D) & bet4(A,B,C,D))=>(bet(B,C,D))))).

fof(th_3_11_1,axiom,(![A,B,C,P]:((point(A) & point(B) & point(C) & point(P) & bet(A,B,C)&bet(A,P,B))=>bet4(A,P,B,C)))).

fof(th_3_11_2,axiom,(![A,B,C,P]:((point(A) & point(B) & point(C) & point(P) & bet(A,B,C)&bet(B,P,C))=>bet4(A,B,P,C)))).

fof(th_3_12_1,axiom,(![A1,A2,A3,P]:((point(A1) & point(A2) & point(A3) & point(P) & bet(A1,A2,A3)&bet(A2,A3,P)&A2!=A3)=>(bet4(A1,A2,A3,P))))).

fof(th_3_12_2,axiom,(![A1,A2,A3,P]:((point(A1) & point(A2) & point(A3) & point(P) & bet(A1,A2,A3)&bet(A1,A3,P))=>(bet4(A1,A2,A3,P))))).

fof(th_3_13,axiom,(?[A,B]:((A!=B)))).

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

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

fof(th_3_15_2,axiom,(![A,B]:((point(A) & point(B) & A!=B)=>(?[C,D]:(bet4(A,B,C,D)&A!=C&A!=D&B!=C&B!=D&C!=D))))).

fof(th_3_17,axiom,(![A,B,C,A1,B1,P]:((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(P) & bet(A,B,C)&bet(A1,B1,C)&bet(A,P,A1))=>(?[Q]:(bet(P,Q,C)&bet(B,Q,B1)))))).

fof(ax_4_1_1,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & ifs(A,B,C,D,A1,B1,C1,D1))=>(bet(A,B,C)&bet(A1,B1,C1)&cong(A,C,A1,C1)&cong(B,C,B1,C1)&cong(A,D,A1,D1)&cong(C,D,C1,D1))))).

fof(ax_4_1_2,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & bet(A,B,C)&bet(A1,B1,C1)&cong(A,C,A1,C1)&cong(B,C,B1,C1)&cong(A,D,A1,D1)&cong(C,D,C1,D1))=>(ifs(A,B,C,D,A1,B1,C1,D1))))).

fof(ax_branch_ifs,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & ) => (ifs(A,B,C,D,A1,B1,C1,D1)|nifs(A,B,C,D,A1,B1,C1,D1))))).

fof(ax_false_ifs,axiom,(![A,B,C,D,A1,B1,C1,D1]:((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & ifs(A,B,C,D,A1,B1,C1,D1)&nifs(A,B,C,D,A1,B1,C1,D1))=>$false))).
