%--------------------------------------------------------------------------
% File     : S5LAxioms+1 : TPTP v0.0.0. Released v0.0.0.
% Domain   : Homological Algebra
% Axioms   : Short Five Lemma axioms
% Version  : [TPTP] axioms.
% English  :

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

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

% Comments : 
%--------------------------------------------------------------------------
input_formula(alpha_morphism,axiom,(
    morphism(alpha,a,b)   )).

input_formula(beta_morphism,axiom,(
    morphism(beta,b,c)   )).

input_formula(gamma_morphism,axiom,(
    morphism(gamma,d,e)   )).

input_formula(delta_morphism,axiom,(
    morphism(delta,e,r)   )).

input_formula(f_morphism,axiom,(
    morphism(f,a,d)   )).

input_formula(g_morphism,axiom,(
    morphism(g,b,e)   )).

input_formula(h_morphism,axiom,(
    morphism(h,c,r)   )).

input_formula(alpha_injection,axiom,(
    injection(alpha)   )).

input_formula(gamma_injection,axiom,(
    injection(gamma)   )).

input_formula(beta_surjection,axiom,(
    surjection(beta)   )).

input_formula(delta_surjection,axiom,(
    surjection(delta)   )).

input_formula(alpha_beta_exact,axiom,(
    exact(alpha,beta)   )).

input_formula(gamma_delta_exact,axiom,(
    exact(gammma,delta)   )).

input_formula(alpha_g_f_gamma_commute,axiom,(
    commute(alpha,g,f,gamma)   )).

input_formula(beta_h_g_delta_commute,axiom,(
    commute(beta,h,g,delta)   )).
%--------------------------------------------------------------------------