%--------------------------------------------------------------------------
% File     : GEO004+1 : TPTP v7.2.0. Released v2.4.0.
% Domain   : Geometry (Oriented curves)
% Axioms   : Betweenness for simple curves
% Version  : [EHK99] axioms.
% English  :

% Refs     : [KE99]  Kulik & Eschenbach (1999), A Geometry of Oriented Curv
%          : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% Source   : [EHK99]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :    1 (   0 unit)
%            Number of atoms       :    6 (   1 equality)
%            Maximal formula depth :   11 (  11 average)
%            Number of connectives :    6 (   1 ~  ;   0  |;   4  &)
%                                         (   1 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    5 (   0 propositional; 2-4 arity)
%            Number of functors    :    0 (   0 constant; --- arity)
%            Number of variables   :    5 (   0 singleton;   4 !;   1 ?)
%            Maximal term depth    :    1 (   1 average)
% SPC      : 

% Comments : Requires GEO004+0.ax
%--------------------------------------------------------------------------
fof(between_c_defn,axiom,
    ( ! [C,P,Q,R] :
        ( between_c(C,P,Q,R)
      <=> ( P != R
          & ? [Cpp] :
              ( part_of(Cpp,C)
              & end_point(P,Cpp)
              & end_point(R,Cpp)
              & inner_point(Q,Cpp) ) ) ) )).

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