%--------------------------------------------------------------------------
% 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 clauses    :   14 (   0 non-Horn;   1 unit;  12 RR)
%            Number of atoms      :   29 (   1 equality)
%            Maximal clause size  :    4 (   2 average)
%            Number of predicates :    5 (   0 propositional; 1-3 arity)
%            Number of functors   :    5 (   0 constant; 1-2 arity)
%            Number of variables  :   34 (   2 singleton)
%            Maximal term depth   :    4 (   2 average)
% SPC      : 

% Comments : Requires GEO004-0.ax GEO004-1.ax GEO004-2.ax
%          : Created by tptp2X -f tptp -t clausify:otter GEO004+3.ax
%--------------------------------------------------------------------------
cnf(connect_defn_1,axiom,
    ( ~ connect(A,B,C)
    | once(at_the_same_time(at(A,C),at(B,C))) )).

cnf(connect_defn_2,axiom,
    ( ~ once(at_the_same_time(at(A,B),at(C,B)))
    | connect(A,C,B) )).

cnf(symmetry_of_at_the_same_time_3,axiom,
    ( ~ once(at_the_same_time(A,B))
    | once(at_the_same_time(B,A)) )).

cnf(symmetry_of_at_the_same_time_4,axiom,
    ( ~ once(at_the_same_time(A,B))
    | once(at_the_same_time(B,A)) )).

cnf(assciativity_of_at_the_same_time_5,axiom,
    ( ~ once(at_the_same_time(at_the_same_time(A,B),C))
    | once(at_the_same_time(A,at_the_same_time(B,C))) )).

cnf(assciativity_of_at_the_same_time_6,axiom,
    ( ~ once(at_the_same_time(A,at_the_same_time(B,C)))
    | once(at_the_same_time(at_the_same_time(A,B),C)) )).

cnf(idempotence_of_at_the_same_time_7,axiom,
    ( ~ once(A)
    | once(at_the_same_time(A,A)) )).

cnf(conjunction_at_the_same_time_8,axiom,
    ( ~ once(at_the_same_time(A,B))
    | once(A) )).

cnf(conjunction_at_the_same_time_9,axiom,
    ( ~ once(at_the_same_time(A,B))
    | once(B) )).

cnf(at_on_trajectory_10,axiom,
    ( ~ once(at(A,B))
    | incident_o(B,trajectory_of(A)) )).

cnf(at_on_trajectory_11,axiom,
    ( ~ incident_o(A,trajectory_of(B))
    | once(at(B,A)) )).

cnf(trajectories_are_oriented_curves_12,axiom,
    ( trajectory_of(A) = ax3_sk1(A) )).

cnf(homogeneous_behaviour_13,axiom,
    ( ~ once(at_the_same_time(at(A,B),at(C,D)))
    | ~ once(at_the_same_time(at(A,E),at(C,F)))
    | ~ ordered_by(trajectory_of(A),B,E)
    | ~ ordered_by(trajectory_of(C),F,D) )).

cnf(localization_14,axiom,
    ( ~ once(A)
    | once(at_the_same_time(A,at(B,ax3_sk2(B,A)))) )).

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