% axiom 1, i.e. ax_angle1_1, and ax_angle1_2 in diagram-angle transfer axioms
% based on axiom1 in diagram-segment transfer axioms		
% define predicate right_angle, with Avigad axioms
% defined in ax_angle2 in diagram-angle transfer axioms
% first time uses cong_angle_zero, has equivalence in original Avigads axiom
% it is defined through cong_less so some axioms do not have to be added like A=<B => A+C=<B+C
% the following axiom has if and only if, and we need to split it into two axioms
%"B is on or inside C1" thus we formulate 2 axioms
%Avigad does not use diffside in this axiom
%Avigad mentions oposite = diffside, but does not use it in axiom
%Avigad: This axiom is, in fact, a first-order consequence of the others but is useful in more restrictive notions of consequence - section 3.8
%Avigad: the following axioms Euclid seems to take to be clear form the definitions. They include 0 as a magnitude.
%Euclid postulate 5 - is it part of axioms 
%Euclid postulates and common notions are among these axioms
%as our system does not work with functions, we must add new definitions and rules as axioms; These axioms are almost identical as some Tarski axioms
%avigad says that we can use outside<=>ninside&nonc and that definition can be added as an axiom
%axiom is equivalence, thus we have two
%axiom states ...each inside or on circle... for two points, so we get 4 combinations, i.e. 4 axioms
%axiom states ...inside or on circle... for one point, so we get 2 combinations, i.e. 2 axioms
%fof(ax_branch_diffside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B)) => (diffside(A,B,L) | ndiffside(A,B,L))))).
%fof(ax_branch_outside, axiom, (! [C,A] : ((point(A) & circle(C)) => (outside(A,C) | noutside(A,C))))).
%fof(ax_diffside1, axiom, (! [A,B,L] : ((point(A) & point(B) & line(L) & diffside(A,B,L)) => (non(A,L) & non(B,L) & nsameside(A,B,L))))).
%fof(ax_diffside2, axiom, (! [A,B,L] : ((point(A) & point(B) & line(L) & non(A,L) & non(B,L) & nsameside(A,B,L)) => (diffside(A,B,L))))).
%fof(ax_false_diffside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & diffside(A,B,L) & ndiffside(A,B,L)) => $false))).
%fof(ax_false_outside, axiom, (! [C,A] : ((point(A) & circle(C) & outside(A,C) & noutside(A,C)) => $false))).
%fof(ax_outside1, axiom, (! [A,K] : ((point(A) & circle(K) & ninside(A,K) & nonc(A,K)) => (outside(A,K))))).
%fof(ax_outside2, axiom, (! [A,K] : ((point(A) & circle(K) & outside(A,K)) => (ninside(A,K) & nonc(A,K))))).
%fof(ax_points6, axiom, (! [L,A] : ((line(L) & point(A) & non(A,L)) => (? [B] : (point(B) & non(B,L) & diffside(A,B,L)))))).
%fof(ax_points9, axiom, (! [C] : ((circle(C)) => (? [A] : (point(A) & outside(A,C)))))).   
%fof(ax_samesideAux1,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & non(A,L) & non(B,L) & non(C,L) & diffside(A,B,L) & diffside(A,C,L)) => (sameside(B,C,L))))).
%fof(ax_samesideAux2,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & non(A,L) & non(B,L) & non(C,L) & sameside(A,B,L) & diffside(A,C,L)) => (diffside(B,C,L))))).
%for every predicate R, new predicate nR is introduced with two following axioms per predicate
%the name for the group is chosen to indicate that they provide an analysis of the usual Pasch axiom into more basic diagrammatic rules - page 21 Avigad paper on Elements
%these axioms explain how three lines intersecting in a point divide space into regions
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_angle_add1_1, axiom, (![A,B,C,Z1,Z2,Z3] : ((point(A) & point(B) & point(C) & point(Z1) & point(Z2) & point(Z3) & cong_angle_zero(Z1,Z2,Z3)) => (angle_add(A,B,C,Z1,Z2,Z3,A,B,C))))).
fof(ax_angle_add1_2, axiom, (![A,B,C,Z1,Z2,Z3] : ((point(A) & point(B) & point(C) & point(Z1) & point(Z2) & point(Z3) & angle_add(A,B,C,Z1,Z2,Z3,A,B,C)) => cong_angle_zero(Z1,Z2,Z3)))).
fof(ax_angle_add2, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,D1,D2,D3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(D1) & point(D2) & point(D3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & cong_angle(A1,A2,A3,D1,D2,D3)) => (angle_add(D1,D2,D3,B1,B2,B3,C1,C2,C3))))).
fof(ax_angle_add3, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,D1,D2,D3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(D1) & point(D2) & point(D3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & cong_angle(B1,B2,B3,D1,D2,D3)) => (angle_add(A1,A2,A3,D1,D2,D3,C1,C2,C3))))).
fof(ax_angle_add4, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,D1,D2,D3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(D1) & point(D2) & point(D3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & cong_angle(C1,C2,C3,D1,D2,D3)) => (angle_add(A1,A2,A3,B1,B2,B3,D1,D2,D3))))).
fof(ax_angle_add5, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3)) => (angle_add(B1,B2,B3,A1,A2,A3,C1,C2,C3))))).
fof(ax_angle_add6, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,A4,A5,A6,B4,B5,B6,C4,C5,C6] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(A4) & point(A5) & point(A6) & point(B4) & point(B5) & point(B6) & point(C4) & point(C5) & point(C6) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & angle_add(A4,A5,A6,B4,B5,B6,C4,C5,C6) & cong_angle(A1,A2,A3,A4,A5,A6) & cong_angle(B1,B2,B3,B4,B5,B6)) => (cong_angle(C1,C2,C3,C4,C5,C6))))).
fof(ax_angle_add7, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,A4,A5,A6,B4,B5,B6,C4,C5,C6] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(A4) & point(A5) & point(A6) & point(B4) & point(B5) & point(B6) & point(C4) & point(C5) & point(C6) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & angle_add(A4,A5,A6,B4,B5,B6,C4,C5,C6) & cong_angle(A1,A2,A3,A4,A5,A6) & cong_angle(C1,C2,C3,C4,C5,C6)) => (cong_angle(B1,B2,B3,B4,B5,B6))))).
fof(ax_angle_add8, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,A4,A5,A6,B4,B5,B6,C4,C5,C6] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(A4) & point(A5) & point(A6) & point(B4) & point(B5) & point(B6) & point(C4) & point(C5) & point(C6) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & angle_add(A4,A5,A6,B4,B5,B6,C4,C5,C6) & cong_angle(B1,B2,B3,B4,B5,B6) & cong_angle(C1,C2,C3,C4,C5,C6)) => (cong_angle(A1,A2,A3,A4,A5,A6))))).
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) & A!=B & 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_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, (![A,B,C] : ((point(A) & point(B) & point(C) & col(A,B,C)) => (cong_less(A,B,A,C) & cong_less(B,C,A,C))))).
fof(ax_cong_less2, 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_less3, 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_less4, 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_less5, 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,B] : ((point(A) & point(B) & A=B) => (cong_zero(A,B))))).
fof(ax_metric2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_leq(C,C,A,B))))).
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))))).
