%------------------------------------------------------------------------------
% File     : GRA001+0 : TPTP v7.2.0. Bugfixed v3.2.0.
% Domain   : Graph Theory
% Axioms   : Directed graphs and paths
% Version  : [TPTP] axioms : Especial.
% English  :

% Refs     :
% Source   : [TPTP]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :   12 (   0 unit)
%            Number of atoms       :   72 (  21 equality)
%            Maximal formula depth :   13 (  10 average)
%            Number of connectives :   66 (   6 ~  ;   3  |;  38  &)
%                                         (   2 <=>;  12 =>;   2 <=)
%                                         (   3 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   11 (   1 propositional; 0-3 arity)
%            Number of functors    :    5 (   1 constant; 0-2 arity)
%            Number of variables   :   48 (   0 singleton;  39 !;   9 ?)
%            Maximal term depth    :    2 (   1 average)
% SPC      : 

% Comments :
% Bugfixes : v3.2.0 - Added formula edge_ends_are_vertices.
%------------------------------------------------------------------------------
fof(no_loops,axiom,
    ( ! [E] :
        ( edge(E)
       => head_of(E) != tail_of(E) ) )).

fof(edge_ends_are_vertices,axiom,
    ( ! [E] :
        ( edge(E)
       => ( vertex(head_of(E))
          & vertex(tail_of(E)) ) ) )).

fof(complete_properties,axiom,
    ( complete
   => ! [V1,V2] :
        ( ( vertex(V1)
          & vertex(V2)
          & V1 != V2 )
       => ? [E] :
            ( edge(E)
            & ( ( V1 = head_of(E)
                & V2 = tail_of(E) )
            <~> ( V2 = head_of(E)
                & V1 = tail_of(E) ) ) ) ) )).

fof(path_defn,axiom,
    ( ! [V1,V2,P] :
        ( path(V1,V2,P)
       <= ( vertex(V1)
          & vertex(V2)
          & ? [E] :
              ( edge(E)
              & V1 = tail_of(E)
              & ( ( V2 = head_of(E)
                  & P = path_cons(E,empty) )
                | ? [TP] :
                    ( path(head_of(E),V2,TP)
                    & P = path_cons(E,TP) ) ) ) ) ) )).

fof(path_properties,axiom,
    ( ! [V1,V2,P] :
        ( path(V1,V2,P)
       => ( vertex(V1)
          & vertex(V2)
          & ? [E] :
              ( edge(E)
              & V1 = tail_of(E)
              & ( ( V2 = head_of(E)
                  & P = path_cons(E,empty) )
              <~> ? [TP] :
                    ( path(head_of(E),V2,TP)
                    & P = path_cons(E,TP) ) ) ) ) ) )).

fof(on_path_properties,axiom,
    ( ! [V1,V2,P,E] :
        ( ( path(V1,V2,P)
          & on_path(E,P) )
       => ( edge(E)
          & in_path(head_of(E),P)
          & in_path(tail_of(E),P) ) ) )).

fof(in_path_properties,axiom,
    ( ! [V1,V2,P,V] :
        ( ( path(V1,V2,P)
          & in_path(V,P) )
       => ( vertex(V)
          & ? [E] :
              ( on_path(E,P)
              & ( V = head_of(E)
                | V = tail_of(E) ) ) ) ) )).

fof(sequential_defn,axiom,
    ( ! [E1,E2] :
        ( sequential(E1,E2)
      <=> ( edge(E1)
          & edge(E2)
          & E1 != E2
          & head_of(E1) = tail_of(E2) ) ) )).

fof(precedes_defn,axiom,
    ( ! [P,V1,V2] :
        ( path(V1,V2,P)
       => ! [E1,E2] :
            ( precedes(E1,E2,P)
           <= ( on_path(E1,P)
              & on_path(E2,P)
              & ( sequential(E1,E2)
                | ? [E3] :
                    ( sequential(E1,E3)
                    & precedes(E3,E2,P) ) ) ) ) ) )).

fof(precedes_properties,axiom,
    ( ! [P,V1,V2] :
        ( path(V1,V2,P)
       => ! [E1,E2] :
            ( precedes(E1,E2,P)
           => ( on_path(E1,P)
              & on_path(E2,P)
              & ( sequential(E1,E2)
              <~> ? [E3] :
                    ( sequential(E1,E3)
                    & precedes(E3,E2,P) ) ) ) ) ) )).

fof(shortest_path_defn,axiom,
    ( ! [V1,V2,SP] :
        ( shortest_path(V1,V2,SP)
      <=> ( path(V1,V2,SP)
          & V1 != V2
          & ! [P] :
              ( path(V1,V2,P)
             => less_or_equal(length_of(SP),length_of(P)) ) ) ) )).

fof(shortest_path_properties,axiom,
    ( ! [V1,V2,E1,E2,P] :
        ( ( shortest_path(V1,V2,P)
          & precedes(E1,E2,P) )
       => ( ~ ( ? [E3] :
                  ( tail_of(E3) = tail_of(E1)
                  & head_of(E3) = head_of(E2) ) )
          & ~ precedes(E2,E1,P) ) ) )).
%------------------------------------------------------------------------------