%------------------------------------------------------------------------------
% File     : GEO007+1 : TPTP v7.2.0. Released v3.3.0.
% Domain   : Geometry (Constructive)
% Axioms   : Principles of a classical calculus of directed lines
% Version  : [vPl98] axioms.
% English  :

% Refs     : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% Source   : [ILTP]
% Names    :

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

% Comments : Requires GEO007+0
% Bugfixes : v6.4.0 - Fixed cld4.
%------------------------------------------------------------------------------
fof(cld1,axiom,(
    ! [L] : ~ unequally_directed_lines(L,L) )).

fof(cld2,axiom,(
    ! [L,M,N] :
      ( ( ~ unequally_directed_lines(L,M)
        & ~ unequally_directed_lines(L,N) )
     => ~ unequally_directed_lines(M,N) ) )).

fof(cld3,axiom,(
    ! [A,B,L,M] :
      ( ~ ( unequally_directed_lines(L,M)
          & unequally_directed_lines(L,reverse_line(M)) )
    <=> ( ~ unequally_directed_lines(L,M)
        | ~ unequally_directed_lines(L,reverse_line(M)) ) ) )).

fof(cld3a,axiom,(
    ! [L,M,N] :
      ( ( ( ~ unequally_directed_lines(L,M)
          | ~ unequally_directed_lines(L,reverse_line(M)) )
        & ( ~ unequally_directed_lines(L,N)
          | ~ unequally_directed_lines(L,reverse_line(N)) ) )
     => ( ~ unequally_directed_lines(M,N)
        | ~ unequally_directed_lines(M,reverse_line(N)) ) ) )).

fof(cld4,axiom,(
    ! [L,M] :
      ( ( line(L)
        & line(M) )
     => ~ ( ~ unequally_directed_lines(L,M)
          & ~ unequally_directed_lines(L,reverse_line(M)) ) ) )).

fof(cld5,axiom,(
    ! [L,M,N] :
      ( ~ unequally_directed_lines(L,reverse_line(M))
      & ( ~ unequally_directed_lines(L,reverse_line(N))
       => ~ unequally_directed_lines(M,N) ) ) )).

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