%--------------------------------------------------------------------------
% File     : GEO002-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Geometry (Tarskian)
% Axioms   : Tarski geometry axioms
% Version  : [Qua89] axioms.
% English  :

% Refs     : [Tar59] Tarski (1959), What is Elementary Geometry?
%          : [MOW76] McCharen et al. (1976), Problems and Experiments for a
%          : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% Source   : [ANL]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :   18 (   5 non-Horn;   6 unit;  15 RR)
%            Number of atoms      :   56 (   7 equality)
%            Maximal clause size  :    8 (   3 average)
%            Number of predicates :    3 (   0 propositional; 2-4 arity)
%            Number of functors   :    8 (   3 constant; 0-6 arity)
%            Number of variables  :   71 (   3 singleton)
%            Maximal term depth   :    2 (   1 average)
% SPC      : 

% Comments : See [Qua89] p.100, for details of the differences from the
%            [MOW76] axioms.
%          : Skolem functions are:
%                inner_pasch : From Inner Pasch Axiom (A7)
%                euclid1     : From Euclid's Axiom (A8)
%                euclid2     : From Euclid's Axiom (A8)
%                extend      : From the Segment Construction Axiom (A10)
%                continuous  : From the Weakened form of the Elementary
%                              Continuity Axiom (A13')
%--------------------------------------------------------------------------
%----A1 - Reflexivity axiom for equidistance
cnf(reflexivity_for_equidistance,axiom,
    ( equidistant(X,Y,Y,X) )).

%----A2 - Transitivity axiom for equidistance
cnf(transitivity_for_equidistance,axiom,
    ( ~ equidistant(X,Y,Z,V)
    | ~ equidistant(X,Y,V2,W)
    | equidistant(Z,V,V2,W) )).

%----A3 Indentity axiom for equidistance
cnf(identity_for_equidistance,axiom,
    ( ~ equidistant(X,Y,Z,Z)
    | X = Y )).

%----A4 - Segment construction axiom, two clauses.
%----A4.1
cnf(segment_construction1,axiom,
    ( between(X,Y,extension(X,Y,W,V)) )).

%----A4.2
cnf(segment_construction2,axiom,
    ( equidistant(Y,extension(X,Y,W,V),W,V) )).

%----A5 - Outer five-segment axiom
cnf(outer_five_segment,axiom,
    ( ~ equidistant(X,Y,X1,Y1)
    | ~ equidistant(Y,Z,Y1,Z1)
    | ~ equidistant(X,V,X1,V1)
    | ~ equidistant(Y,V,Y1,V1)
    | ~ between(X,Y,Z)
    | ~ between(X1,Y1,Z1)
    | X = Y
    | equidistant(Z,V,Z1,V1) )).

%----A6 - Identity axiom for betweenness
cnf(identity_for_betweeness,axiom,
    ( ~ between(X,Y,X)
    | X = Y )).

%----A7 - Inner Pasch axiom, two clauses.
%----A7.1
cnf(inner_pasch1,axiom,
    ( ~ between(U,V,W)
    | ~ between(Y,X,W)
    | between(V,inner_pasch(U,V,W,X,Y),Y) )).

%----A7.2
cnf(inner_pasch2,axiom,
    ( ~ between(U,V,W)
    | ~ between(Y,X,W)
    | between(X,inner_pasch(U,V,W,X,Y),U) )).

%----A8 - Lower dimension axiom, three clauses.
%----A8.1
cnf(lower_dimension1,axiom,
    ( ~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) )).

%----A8.2
cnf(lower_dimension2,axiom,
    ( ~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1) )).

%----A8.3
cnf(lower_dimension3,axiom,
    ( ~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2) )).

%----A9 - Upper dimension axiom
cnf(upper_dimension,axiom,
    ( ~ equidistant(X,W,X,V)
    | ~ equidistant(Y,W,Y,V)
    | ~ equidistant(Z,W,Z,V)
    | between(X,Y,Z)
    | between(Y,Z,X)
    | between(Z,X,Y)
    | W = V )).

%----A10 - Euclid's axiom, three clauses.
%----A10.1
cnf(euclid1,axiom,
    ( ~ between(U,W,Y)
    | ~ between(V,W,X)
    | U = W
    | between(U,V,euclid1(U,V,W,X,Y)) )).

%----A10.2
cnf(euclid2,axiom,
    ( ~ between(U,W,Y)
    | ~ between(V,W,X)
    | U = W
    | between(U,X,euclid2(U,V,W,X,Y)) )).

%----A10.3
cnf(euclid3,axiom,
    ( ~ between(U,W,Y)
    | ~ between(V,W,X)
    | U = W
    | between(euclid1(U,V,W,X,Y),Y,euclid2(U,V,W,X,Y)) )).

%----A11 - Weakened continuity axiom, two clauses.
%----A11.1
cnf(continuity1,axiom,
    ( ~ equidistant(U,V,U,V1)
    | ~ equidistant(U,X,U,X1)
    | ~ between(U,V,X)
    | ~ between(V,W,X)
    | between(V1,continuous(U,V,V1,W,X,X1),X1) )).

%----A11.2
cnf(continuity2,axiom,
    ( ~ equidistant(U,V,U,V1)
    | ~ equidistant(U,X,U,X1)
    | ~ between(U,V,X)
    | ~ between(V,W,X)
    | equidistant(U,W,U,continuous(U,V,V1,W,X,X1)) )).

%--------------------------------------------------------------------------