%------------------------------------------------------------------------------
% File     : GEO011+0 : TPTP v7.2.0. Released v7.0.0.
% Domain   : Geometry
% Axioms   : Tarskian geometry
% Version  : [Urb16] axioms : Especial.
% English  :

% Refs     : [Urb16] Urban (2016), Email to Geoff Sutcliffe
%          : [BW17]  Beeson & Wos (2017), Finding Proofs in Tarskian Geomet
% Source   : [Urb16]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :    8 (   1 unit)
%            Number of atoms       :   27 (   3 equality)
%            Maximal formula depth :   16 (   8 average)
%            Number of connectives :   36 (  17   ~;  15   |;   4   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of predicates  :    3 (   0 propositional; 2-4 arity)
%            Number of functors    :    5 (   3 constant; 0-5 arity)
%            Number of variables   :   30 (   0 sgn;  30   !;   0   ?)
%            Maximal term depth    :    2 (   1 average)
% SPC      : FOF_SAT_RFO_SEQ

% Comments :
%------------------------------------------------------------------------------
fof(aA1,axiom,(
    ! [X,Y] : s_e(X,Y,Y,X) )).

fof(aA2,axiom,(
    ! [X,Y,Z,V,Z2,V2] :
      ( ~ s_e(X,Y,Z,V)
      | ~ s_e(X,Y,Z2,V2)
      | s_e(Z,V,Z2,V2) ) )).

fof(aA3,axiom,(
    ! [X,Y,Z] :
      ( ~ s_e(X,Y,Z,Z)
      | X = Y ) )).

fof(aA4,axiom,(
    ! [X,Y,W,V] :
      ( s_t(X,Y,ext(X,Y,W,V))
      & s_e(Y,ext(X,Y,W,V),W,V) ) )).

fof(aA5,axiom,(
    ! [X,Y,X1,Y1,Z,Z1,V,V1] :
      ( ~ s_e(X,Y,X1,Y1)
      | ~ s_e(Y,Z,Y1,Z1)
      | ~ s_e(X,V,X1,V1)
      | ~ s_e(Y,V,Y1,V1)
      | ~ s_t(X,Y,Z)
      | ~ s_t(X1,Y1,Z1)
      | X = Y
      | s_e(Z,V,Z1,V1) ) )).

fof(aA6,axiom,(
    ! [X,Y] :
      ( ~ s_t(X,Y,X)
      | X = Y ) )).

fof(aA7,axiom,(
    ! [Xa,Xp,Xc,Xb,Xq] :
      ( ( ~ s_t(Xa,Xp,Xc)
        | ~ s_t(Xb,Xq,Xc)
        | s_t(Xp,ip(Xa,Xp,Xc,Xb,Xq),Xb) )
      & ( ~ s_t(Xa,Xp,Xc)
        | ~ s_t(Xb,Xq,Xc)
        | s_t(Xq,ip(Xa,Xp,Xc,Xb,Xq),Xa) ) ) )).

fof(aA8,axiom,
    ( ~ s_t(alpha,beta,gamma)
    & ~ s_t(beta,gamma,alpha)
    & ~ s_t(gamma,alpha,beta) )).

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