fof(ax_angle1_1, axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & A != B & A != C & on(A,L) & on(B,L) & on(C,L) & nbet(B,A,C)) => (cong_angle_zero(B,A,C))))).
fof(ax_angle1_2, axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & A != B & A != C & on(A,L) & on(B,L) & cong_angle_zero(B,A,C)) => (on(C,L) & nbet(B,A,C))))).
fof(ax_angle2_1, axiom, (! [A,B,C,D,L,M] : ((point(A) & point(B) & point(C) & point(D) & line(L) & line(M) & on(A,L) & on(A,M) & on(B,L) & on(C,M) & A != B & A != C & non(D,L) & non(D,M) & L != M  & angle_add(B,A,D,D,A,C,B,A,C)) => (sameside(B,D,M) & sameside(C,D,L))))).
fof(ax_angle2_2, axiom, (! [A,B,C,D,L,M] : ((point(A) & point(B) & point(C) & point(D) & line(L) & line(M) & on(A,L) & on(A,M) & on(B,L) & on(C,M) & A != B & A != C & non(D,L) & non(D,M) & L != M  & sameside(B,D,M) & sameside(C,D,L)) => (angle_add(B,A,D,D,A,C,B,A,C))))).
fof(ax_angle3_1, axiom, (! [A,B,C,D,L] : ((point(A) & point(B) & point(C) & point(D) & line(L) & on(A,L) & on(B,L) & bet(A,C,B) & non(D,L) & cong_angle(A,C,D,D,C,B)) => (right_angle(A,C,D))))).
fof(ax_angle3_2, axiom, (! [A,B,C,D,L] : ((point(A) & point(B) & point(C) & point(D) & line(L) & on(A,L) & on(B,L) & bet(A,C,B) & non(D,L) & right_angle(A,C,D)) => (cong_angle(A,C,D,D,C,B))))).
fof(ax_angle4, axiom, (! [A,B,B1,C,C1,L,M] : ((point(A) & point(B) & point(B1) & point(C) & point(C1) & line(L) & line(M) & on(A,L) & on(B,L) & on(B1,L) & on(A,M) & on(C,M) & on(C1,M) & B != A & B1 != A & C != A & C1 != A & nbet(B,A,B1) & nbet(C,A,C1)) => (cong_angle(B,A,C,B1,A,C1))))).
fof(ax_angle5, axiom, (! [A,B,C,D,L,M,N,P1,P2,P3,R1,R2,R3,R4,R5,R6,R7,R8,R9,E] : ((point(A) & point(B) & point(C) & point(D) & line(L) & line(M) & line(N) & point(P1) & point(P2) & point(P3) & point(R1) & point(R2) & point(R3) & point(R4) & point(R5) & point(R6) & point(R7) & point(R8) & point(R9) & point(E) & on(A,L) & on(B,L) & on(B,M) & on(C,M) & on(C,N) & on(D,N) & B != C & sameside(A,D,M) & angle_add(A,B,C,B,C,D,P1,P2,P3) & right_angle(R1,R2,R3) & right_angle(R4,R5,R6) & angle_add(R1,R2,R3,R4,R5,R6,R7,R8,R9) & cong_angle_less(P1,P2,P3,R7,R8,R9) & on(E,L) & on(E,N)) => (intersects(L,N) & sameside(E,A,M))))).
fof(ax_area1_1, axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & on(A,L) & on(B,L) & A != B & cong_area_zero(A,B,C)) => (on(C,L))))).
fof(ax_area1_2, axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & on(A,L) & on(B,L) & A != B & on(C,L)) => cong_area_zero(A,B,C)))).
fof(ax_area2_1, axiom, (! [A,B,C,D,L] : ((point(A) & point(B) & point(C) & point(D) & line(L) & on(A,L) & on(B,L) & on(C,L) & A != B & A != C & B != C & non(D,L) & bet(A,C,B)) => (area_add(A,C,D,D,C,B,A,D,B))))).
fof(ax_area2_2, axiom, (! [A,B,C,D,L] : ((point(A) & point(B) & point(C) & point(D) & line(L) & on(A,L) & on(B,L) & on(C,L) & A != B & A != C & B != C & non(D,L) & area_add(A,C,D,D,C,B,A,D,B)) => bet(A,C,B)))).
fof(ax_bet1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & bet(A,B,C)) => (bet(C,B,A) & A != B & A != C & nbet(B,A,C))))).
fof(ax_bet2, axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & bet(A,B,C) & on(A,L) & on(B,L)) => on(C,L)))).
fof(ax_bet3, axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & bet(A,B,C) & on(A,L) & on(C,L)) => on(B,L)))).
fof(ax_bet4, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & bet(A,B,C) & bet(A,D,B)) => bet(A,D,C)))).
fof(ax_bet5, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & bet(A,B,C) & bet(B,C,D)) => bet(A,B,D)))).
fof(ax_bet6,axiom, (! [A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & on(A,L) & on(B,L) & on(C,L) & A != B & A != C & B != C) => (bet(A,B,C) | bet(B,A,C) | bet(A,C,B))))).
fof(ax_bet7, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & bet(A,B,C) & bet(A,B,D)) => nbet(C,B,D)))).
fof(ax_branch_bet, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (bet(A,B,C) | nbet(A,B,C))))).
fof(ax_branch_center, axiom, (! [C,A] : ((circle(C) & point(A)) => (center(A,C) | ncenter(A,C))))).
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_branch_cong_zero, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D)) => (cong_zero(A,B,C,D) | ncong_zero(A,B,C,D))))).
fof(ax_branch_inside, axiom, (! [C,A] : ((point(A) & circle(C)) => (inside(A,C) | ninside(A,C))))).
fof(ax_branch_on, axiom, (! [L,A] : ((line(L) & point(A)) => (on(A,L) | non(A,L))))).
fof(ax_branch_onc, axiom, (! [C,A] : ((circle(C) & point(A)) => (onc(A,C) | nonc(A,C))))).
fof(ax_branch_sameside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B)) => (sameside(A,B,L) | nsameside(A,B,L))))).
fof(ax_branch_segment_add, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F)) => (segment_add(A,B,C,D,E,F) | nsegment_add(A,B,C,D,E,F))))).
fof(ax_circle1, axiom, (! [A,B,C,L,P] : ((point(A) & point(B) & point(C) & line(L) & circle(P) & on(A,L) & on(B,L) & on(C,L) & inside(A,P) & onc(B,P) & onc(C,P) & B != C) => (bet(B,A,C))))).
fof(ax_circle2_1, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & inside(A,P) & inside(B,P) & bet(A,C,B)) => (inside(C,P))))).
fof(ax_circle2_2, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & inside(A,P) & onc(B,P) & bet(A,C,B)) => (inside(C,P))))).
fof(ax_circle2_3, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & onc(A,P) & inside(B,P) & bet(A,C,B)) => (inside(C,P))))).
fof(ax_circle2_4, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & onc(A,P) & onc(B,P) & bet(A,C,B)) => (inside(C,P))))).
fof(ax_circle3_1, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & inside(A,P) & ninside(C,P) & bet(A,C,B)) => (ninside(B,P) & nonc(B,P))))).
fof(ax_circle3_2, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & onc(A,P) & ninside(C,P) & bet(A,C,B)) => (ninside(B,P) & nonc(B,P))))).
fof(ax_circle4, axiom, (! [P1,P2,C,D,A,B,L] : ((circle(P1) & circle(P2) & point(C) & point(D) & point(A) & point(B) & line(L) & P1 != P2 & intersectscc(P1,P2) & C != D & onc(C,P1) & onc(C,P2) & onc(D,P1) & onc(D,P2) & center(A,P1) & center(B,P2) & on(A,L) & on(B,L)) => (nsameside(C,D,L))))).
fof(ax_cong_angle_less, axiom, (! [A,B,C,D,E,F,P,Q,R] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & point(P) & point(Q) & point(R) & angle_add(A,B,C,D,E,F,P,Q,R)) => (cong_angle_less(A,B,C,P,Q,R) & cong_angle_less(D,E,F,P,Q,R))))).
fof(ax_cong_angle_reflexivity, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_angle(A,B,C,A,B,C))))).
fof(ax_cong_angle_symmetry, axiom, (! [A,B,C,A1,B1,C1] : ((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(C1) & cong_angle(A,B,C,A1,B1,C1)) => (cong_angle(A1,B1,C1,A,B,C))))).
fof(ax_cong_angle_transitivity, axiom, (! [A,B,C,A1,B1,C1,A2,B2,C2] : ((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(C1) & cong_angle(A,B,C,A1,B1,C1) & cong_angle(A,B,C,A2,B2,C2)) => (cong_angle(A1,B1,C1,A2,B2,C2))))).
fof(ax_cong_eq1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong(A,A,B,C)) => (B=C)))).
fof(ax_cong_leq1, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_leq(A,B,C,D)) => (cong(A,B,C,D) | cong_less(A,B,C,D))))).
fof(ax_cong_leq2, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)) => (cong_leq(A,B,C,D))))).
fof(ax_cong_leq3, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_less(A,B,C,D)) => (cong_leq(A,B,C,D))))).
fof(ax_cong_less1, axiom, (![A1,A2,B1,B2,C1,C2] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & segment_add(A1,A2,B1,B2,C1,C2)) => (cong_less(A1,A2,C1,C2) & cong_less(B1,B2,C1,C2))))).
fof(ax_cong_less2, axiom, (! [A,B,C,D,E,F,G,H,K,L] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & point(G) & point(H) & point(K) & point(L) & cong_less(A,B,C,D) & segment_add(A,B,E,F,G,H) & segment_add(C,D,E,F,K,L)) => (cong_less(G,H,K,L))))).
fof(ax_cong_less3, axiom, (! [A,B,C,D,A1,B1] : ((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & cong_less(A,B,C,D) & cong(A,B,A1,B1)) => (cong_less(A1,B1,C,D))))).
fof(ax_cong_less4, axiom, (! [A,B,C,D,C1,D1] : ((point(A) & point(B) & point(C) & point(D) & point(C1) & point(D1) & cong_less(A,B,C,D) & cong(C,D,C1,D1)) => (cong_less(A,B,C1,D1))))).
fof(ax_cong_reflexivity, axiom, (! [A,B] : ((point(A) & point(B)) => (cong(A,B,A,B))))).
fof(ax_cong_symmetry, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)) => (cong(C,D,A,B))))).
fof(ax_cong_transitivity, 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_cong_zero1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong(A,B,C,C)) => cong_zero(A,B)))).
fof(ax_cong_zero2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong_zero(A,B)) => cong(A,B,C,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_false_center, axiom, (! [C,A] : ((circle(C) & point(A) & center(A,C) & ncenter(A,C)) => $false))).
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_false_cong_zero, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_zero(A,B,C,D) & ncong_zero(A,B,C,D)) => $false))).
fof(ax_false_inside, axiom, (! [C,A] : ((point(A) & circle(C) & inside(A,C) & ninside(A,C)) => $false))).
fof(ax_false_on, axiom, (! [L,A] : ((line(L) & point(A) & on(A,L) & non(A,L)) => $false))).
fof(ax_false_onc, axiom, (! [C,A] : ((circle(C) & point(A) & onc(A,C) & nonc(A,C)) => $false))).
fof(ax_false_sameside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & sameside(A,B,L) & nsameside(A,B,L)) => $false))).
fof(ax_false_segment_add, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & segment_add(A,B,C,D,E,F) & nsegment_add(A,B,C,D,E,F)) => $false))).
fof(ax_generalities1, axiom, (! [A,B,L,M] : ((point(A) & point(B) & line(L) & line(M) & A != B & on(A,L) & on(B,L) & on(A,M) & on(B,M)) => L = M))).
fof(ax_generalities2, axiom, (! [A,B,C] : ((point(A) & point(B) & circle(C) & center(A,C) & center(B,C)) => A = B))).
fof(ax_generalities3, axiom, (! [A,C] : ((point(A) & circle(C) & center(A,C)) => inside(A,C)))).
fof(ax_generalities4, axiom, (! [A,C] : ((point(A) & circle(C) & center(A,C)) => nonc(A,C)))).
fof(ax_incidence1, axiom, (! [L,M,N,A,B,C,D] : ((line(L) & line(M) & line(N) & point(A) & point(B) & point(C) & point(D) & on(A,L) & on(A,M) & on(A,N) & on(B,L) & on(C,M) & on(D,N) & sameside(C,D,L) & sameside(B,C,N)) => (nsameside(B,D,M))))).
fof(ax_incidence2, axiom, (! [L,M,N,A,B,C,D] : ((line(L) & line(M) & line(N) & point(A) & point(B) & point(C) & point(D) & on(A,L) & on(A,M) & on(A,N) & on(B,L) & on(C,M) & on(D,N) & sameside(C,D,L) & nsameside(B,D,M) & non(D,M) & B != A) => (sameside(B,C,N))))).
fof(ax_incidence3, axiom, (! [L,M,N,A,B,C,D,E] : ((line(L) & line(M) & line(N) & point(A) & point(B) & point(C) & point(D) & point(E) & on(A,L) & on(A,M) & on(A,N) & on(B,L) & on(C,M) & on(D,N) & sameside(C,D,L) & sameside(B,C,N) & sameside(D,E,M) & sameside(C,E,N)) => (sameside(C,E,L))))).
fof(ax_intersections1, axiom, (! [L,M] : ((line(L) & line(M) & intersects(L,M)) => (? [A] : (point(A) & on(A,L) & on(A,M)))))).
fof(ax_intersections2, axiom, (! [C,M] : ((circle(C) & line(M) & intersectslc(M,C)) => (? [A] : (point(A) & on(A,M) & onc(A,C)))))).
fof(ax_intersections3, axiom, (! [C,M] : ((circle(C) & line(M) & intersectslc(M,C)) => (? [A,B] : (point(A) & point(B) & on(A,M) & onc(A,C) & on(B,M) & onc(B,C) & A != B))))).
fof(ax_intersections4, axiom, (! [C,L,B,D] : ((circle(C) & line(L) & point(B) & point(D) & inside(B,C) & on(B,L) & ninside(D,C) & nonc(D,C) & on(D,L)) => (? [A] : (point(A) & onc(A,C) & on(A,L) & bet(B,A,D)))))).
fof(ax_intersections5, axiom, (! [C,L,B,D] : ((circle(C) & line(L) &  point(B) & point(D) & inside(B,C) & on(B,L) & D != B & on(D,L)) => (? [A] : (point(A) & onc(A,C) & on(A,L) & bet(A,B,D)))))).
fof(ax_intersections6, axiom, (! [C1,C2] : ((circle(C1) & circle(C2) & intersectscc(C1,C2)) => (? [A] : (point(A) & onc(A,C1) & onc(A,C2)))))).
fof(ax_intersections7, axiom, (! [C1,C2] : ((circle(C1) & circle(C2) & intersectscc(C1,C2)) => (? [A,B] : (point(A) & point(B) & onc(A,C1) & onc(A,C2) & onc(B,C1) & onc(B,C2) & A != B))))).
fof(ax_intersections8, axiom, (! [C1,C2,D1,D2,B,L] : ((circle(C1) & circle(C2) & line(L) & point(D1) & point(D2) & point(B) & intersectscc(C1,C2) & center(D1,C1) & center(D2,C2) & on(D1,L) & on(D2,L) & non(B,L)) => (? [A] : (point(A) & onc(A,C1) & onc(A,C2) & sameside(A,B,L)))))).
fof(ax_intersections9, axiom, (! [C1,C2,D1,D2,B,L] : ((circle(C1) & circle(C2) & point(D1) & point(D2) & point(B) & line(L) & intersectscc(C1,C2) & center(D1,C1) & center(D2,C2) & on(D1,L) & on(D2,L) & non(B,L)) => (? [A] : (point(A) & onc(A,C1) & onc(A,C2) & nsameside(A,B,L) & non(A,L)))))).
fof(ax_lines_and_circles1, axiom, (! [A,B] : ((point(A) & point(B) & A != B) => (? [L] : (line(L) & on(A,L) & on(B,L)))))).
fof(ax_lines_and_circles2, axiom, (! [A,B] : ((point(A) & point(B) & A != B) => (? [C] : (circle(C) & center(A,C) & onc(B,C)))))).
fof(ax_metric1_1, axiom, (! [A,B] : ((point(A) & point(B) & cong_zero(A,B)) => (A=B)))).
fof(ax_metric1_2, axiom, (! [A] : ((point(A)) => (cong_zero(A,A))))).
fof(ax_metric2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_leq(A,A,B,C))))).
fof(ax_metric3, axiom, (! [A,B] : ((point(A) & point(B)) => (cong(A,B,B,A))))).
fof(ax_metric4, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & A != B & A != C) => (cong_angle(A,B,C,C,B,A))))).
fof(ax_metric5_1, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong_angle_zero(A,B,C)) => (cong_angle_leq(A,B,C,D,E,F))))).
fof(ax_metric5_2, axiom, (! [A,B,C,R1,R2,R3,P1,P2,P3,Q1,Q2,Q3] : ((point(A) & point(B) & point(C) & point(R1) & point(R2) & point(R3) & point(P1) & point(P2) & point(P3) & point(Q1) & point(Q2) & point(Q3) & right_angle(R1,R2,R3) & right_angle(P1,P2,P3) & angle_add(R1,R2,R3,P1,P2,P3,Q1,Q2,Q3)) => (cong_angle_leq(A,B,C,Q1,Q2,Q3))))).
fof(ax_metric6, axiom, (! [A,B] : ((point(A) & point(B)) => (cong_area_zero(A,A,B))))).
fof(ax_metric7, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong_area_zero(A,B,C)) => (cong_area_leq(A,B,C,D,E,F))))).
fof(ax_metric8, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_area(A,B,C,C,A,B) & cong_area(A,B,C,A,C,B))))).
fof(ax_metric9, axiom, (! [A,B,C,A1,B1,C1] : ((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(C1) & cong(A,B,A1,B1) & cong(B,C,B1,C1) & cong(C,A,C1,A1) & cong_angle(A,B,C,A1,B1,C1) & cong_angle(B,C,A,B1,C1,A1) & cong_angle(C,A,B,C1,A1,B1)) => (cong_area(A,B,C,A1,B1,C1))))).
fof(ax_pasch1,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & bet(A,B,C) & sameside(A,C,L)) => sameside(A,B,L)))).
fof(ax_pasch2,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & bet(A,B,C) & on(A,L) & non(B,L)) => sameside(B,C,L)))).
fof(ax_pasch3,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & bet(A,B,C) & on(B,L)) => nsameside(A,C,L)))).
fof(ax_pasch4,axiom, (![A,B,C,L,M] : ((point(A) & point(B) & point(C) & line(L) & line(M) & A != B & B != C & L != M & on(A,M) & on(B,M) & on(C,M) & nsameside(A,C,L) & on(B,L)) => bet(A,B,C)))).
fof(ax_points1, axiom, (? [A] : (point(A)))).
fof(ax_points2, axiom, (! [L] : ((line(L)) => (? [A] : (point(A) & on(A,L)))))).
fof(ax_points3, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & on(A,L) & on(B,L) & A != B) => (? [C] : (point(C) & on(C,L) & bet(A,C,B)))))).
fof(ax_points4, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & on(A,L) & on(B,L) & A != B) => (? [C] : (point(C) & on(C,L) & bet(A,B,C)))))).
fof(ax_points5, axiom, (! [L,A] : ((line(L) & point(A) & non(A,L)) => (? [B] : (point(B) & sameside(A,B,L)))))).
fof(ax_points6, axiom, (! [L,A] : ((line(L) & point(A) & non(A,L)) => (? [B] : (point(B) & non(B,L) & nsameside(A,B,L)))))).
fof(ax_points7, axiom, (! [C] : ((circle(C)) => (? [A] : (point(A) & onc(A,C)))))).
fof(ax_points8, axiom, (! [C] : ((circle(C)) => (? [A] : (point(A) & inside(A,C)))))).
fof(ax_points9, axiom, (! [C] : ((circle(C)) => (? [A] : (point(A) & ninside(A,C) & nonc(A,C)))))).
fof(ax_postulate4, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & right_angle(A,B,C) & right_angle(D,E,F)) => (cong_angle(A,B,C,D,E,F))))).
fof(ax_rule1, axiom, (! [A,B,L,M] : ((point(A) & point(B) & line(L) & line(M) & non(A,L) & non(B,L) & nsameside(A,B,L) & on(A,M) & on(B,M)) => (intersects(L,M))))).
fof(ax_rule2_1, axiom, (! [A,B,C,L] : ((point(A) & point(B) & circle(C) & line(L) & onc(A,C) & onc(B,C) & non(A,L) & non(B,L) & nsameside(A,B,L)) => (intersectslc(L,C))))).
fof(ax_rule2_2, axiom, (! [A,B,C,L] : ((point(A) & point(B) & circle(C) & line(L) & onc(A,C) & inside(B,C) & non(A,L) & non(B,L) & nsameside(A,B,L)) => (intersectslc(L,C))))).
fof(ax_rule2_3, axiom, (! [A,B,C,L] : ((point(A) & point(B) & circle(C) & line(L) & inside(A,C) & onc(B,C) & non(A,L) & non(B,L) & nsameside(A,B,L)) => (intersectslc(L,C))))).
fof(ax_rule2_4, axiom, (! [A,B,C,L] : ((point(A) & point(B) & circle(C) & line(L) & inside(A,C) & inside(B,C) & non(A,L) & non(B,L) & nsameside(A,B,L)) => (intersectslc(L,C))))).
fof(ax_rule3, axiom, (! [A,C,L] : ((point(A) & circle(C) & line(L) & inside(A,C) & on(A,L)) => (intersectslc(L,C))))).
fof(ax_rule4_1, axiom, (! [A,B,C1,C2] : ((point(A) & point(B) & circle(C1) & circle(C2) & onc(A,C1) & onc(B,C1) & inside(A,C2) & nonc(B,C2) & ninside(B,C2)) => (intersectscc(C1,C2))))).
fof(ax_rule4_2, axiom, (! [A,B,C1,C2] : ((point(A) & point(B) & circle(C1) & circle(C2) & onc(A,C1) & inside(B,C1) & inside(A,C2) & nonc(B,C2) & ninside(B,C2)) => (intersectscc(C1,C2))))).
fof(ax_rule5, axiom, (! [A,B,C1,C2] : ((point(A) & point(B) & circle(C1) & circle(C2) & onc(A,C1) & inside(B,C1) & inside(A,C2) & onc(B,C2)) => (intersectscc(C1,C2))))).
fof(ax_sameside1,axiom, (![A,L] : ((point(A) & line(L) & non(A,L)) => sameside(A,A,L)))).
fof(ax_sameside2,axiom, (![A,B,L] : ((point(A) & point(B) & line(L) & sameside(A,B,L)) => (sameside(B,A,L))))).
fof(ax_sameside3,axiom, (![A,B,L] : ((point(A) & point(B) & line(L) & sameside(A,B,L)) => (non(A,L))))).
fof(ax_sameside4,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & sameside(A,B,L) & sameside(A,C,L)) => sameside(B,C,L)))).
fof(ax_sameside5,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & non(A,L) & non(B,L) & non(C,L) & nsameside(A,B,L)) => (sameside(A,C,L) | sameside(B,C,L))))).
fof(ax_segment1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & bet(A,B,C)) => (segment_add(A,B,B,C,A,C))))).
fof(ax_segment2, axiom, (! [A,B,C,P1,P2] : ((point(A) & point(B) & point(C) & circle(P1) & circle(P2) & center(A,P1) & center(A,P2) & onc(B,P1) & onc(C,P2) & cong(A,B,A,C)) => (P1 = P2)))).
fof(ax_segment3_1, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & center(A,P) & onc(B,P) & cong(A,C,A,B)) => (onc(C,P))))).
fof(ax_segment3_2, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & center(A,P) & onc(B,P) & onc(C,P)) => (cong(A,C,A,B))))).
fof(ax_segment4_1, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & center(A,P) & onc(B,P) & cong_less(A,C,A,B)) => (inside(C,P))))).
fof(ax_segment4_2, axiom, (! [A,B,C,P] : ((point(A) & point(B) & point(C) & circle(P) & center(A,P) & onc(B,P) & inside(C,P)) => (cong_less(A,C,A,B))))).
fof(ax_segment_add1, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(A1,A2,P,Q)) => (segment_add(P,Q,B1,B2,C1,C2))))).
fof(ax_segment_add2, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(B1,B2,P,Q)) => (segment_add(A1,A2,P,Q,C1,C2))))).
fof(ax_segment_add3, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(C1,C2,P,Q)) => (segment_add(A1,A2,B1,B2,P,Q))))).
fof(ax_segment_add4, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2)) => (segment_add(B1,B2,A1,A2,C1,C2))))).
fof(ax_segment_add5, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_zero(C,D)) => (segment_add(A,B,C,D,A,B) & segment_add(C,D,A,B,A,B))))).
fof(ax_segment_add6, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(A,B,A1,B1) & cong(C,D,C1,D1)) => (cong(P,Q,P1,Q1))))).
fof(ax_segment_add7, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(A,B,A1,B1) & cong(P,Q,P1,Q1)) => (cong(C,D,C1,D1))))).
fof(ax_segment_add8, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(C,D,C1,D1)& cong(P,Q,P1,Q1)) => (cong(A,B,A1,B1))))).
fof(ax_superposition1, axiom, (![A,B,C,D,G,H,L] : ((point(A) & point(B) & point(C) & point(D) & point(G) & point(H) & line(L) & ncol(A,B,C) & A!=B & A!=C & B!=C & D!=G & on(D,L) & on(G,L) & non(H,L)) => (? [A1,B1,C1] : (point(A1) & point(B1) & point(C1) & A1=D & C1!=B & C1!=A & cong_angle(B,A,C,B1,A1,C1) & cong_angle(A,C,B,A1,C1,B1) & cong_angle(C,B,A,C1,B1,A1) & cong(A,B,A1,B1) & cong(B,C,B1,C1) & cong(C,A,C1,A1) & on(B1,L) & nbet(B1,A1,G) & sameside(C1,H,L) & B1!=C1 & A1!=C1))))).
