%--------------------------------------------------------------------------
% File     : GEO004+3 : TPTP v7.2.0. Released v2.4.0.
% Domain   : Geometry (Oriented curves)
% Axioms   : Trajectories
% 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    :    9 (   1 unit)
%            Number of atoms       :   20 (   1 equality)
%            Maximal formula depth :   10 (   5 average)
%            Number of connectives :   12 (   1 ~  ;   0  |;   3  &)
%                                         (   4 <=>;   4 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    5 (   0 propositional; 1-3 arity)
%            Number of functors    :    3 (   0 constant; 1-2 arity)
%            Number of variables   :   24 (   0 singleton;  22 !;   2 ?)
%            Maximal term depth    :    3 (   2 average)
% SPC      : 

% Comments : Requires GEO004+0.ax GEO004+1.ax GEO004+2.ax
%--------------------------------------------------------------------------
fof(connect_defn,axiom,
    ( ! [X,Y,P] :
        ( connect(X,Y,P)
      <=> once(at_the_same_time(at(X,P),at(Y,P))) ) )).

fof(symmetry_of_at_the_same_time,axiom,
    ( ! [A,B] :
        ( once(at_the_same_time(A,B))
      <=> once(at_the_same_time(B,A)) ) )).

fof(assciativity_of_at_the_same_time,axiom,
    ( ! [A,B,C] :
        ( once(at_the_same_time(at_the_same_time(A,B),C))
      <=> once(at_the_same_time(A,at_the_same_time(B,C))) ) )).

fof(idempotence_of_at_the_same_time,axiom,
    ( ! [A] :
        ( once(A)
       => once(at_the_same_time(A,A)) ) )).

fof(conjunction_at_the_same_time,axiom,
    ( ! [A,B] :
        ( once(at_the_same_time(A,B))
       => ( once(A)
          & once(B) ) ) )).

fof(at_on_trajectory,axiom,
    ( ! [X,P] :
        ( once(at(X,P))
      <=> incident_o(P,trajectory_of(X)) ) )).

fof(trajectories_are_oriented_curves,axiom,
    ( ! [X] :
      ? [O] : trajectory_of(X) = O )).

fof(homogeneous_behaviour,axiom,
    ( ! [P1,P2,Q1,Q2,X,Y] :
        ( ( once(at_the_same_time(at(X,P1),at(Y,P2)))
          & once(at_the_same_time(at(X,Q1),at(Y,Q2))) )
       => ~ ( ordered_by(trajectory_of(X),P1,Q1)
            & ordered_by(trajectory_of(Y),Q2,P2) ) ) )).

fof(localization,axiom,
    ( ! [A] :
        ( once(A)
       => ! [X] :
          ? [P] : once(at_the_same_time(A,at(X,P))) ) )).

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