%------------------------------------------------------------------------------
% File     : REL001-0 : TPTP v7.2.0. Released v3.6.0.
% Domain   : Relation Algebra
% Axioms   : Relation algebra
% Version  : [Mad95] (equational) axioms.
% English  :

% Refs     : [Mad95] Maddux (1995), Relation-Algebraic Semantics
%          : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% Source   : [Hoe08]
% Names    :

% Status   : Satisfiable
% Rating   : ? v3.6.0
% Syntax   : Number of clauses     :   13 (   0 non-Horn;  13 unit;   0 RR)
%            Number of atoms       :   13 (  13 equality)
%            Maximal clause size   :    1 (   1 average)
%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
%            Number of functors    :    8 (   3 constant; 0-2 arity)
%            Number of variables   :   25 (   0 singleton)
%            Maximal term depth    :    5 (   3 average)
% SPC      : 

% Comments : tptp2X -f tptp:short -t cnf:otter REL001+0.ax
%------------------------------------------------------------------------------
cnf(maddux1_join_commutativity_1,axiom,
    ( join(A,B) = join(B,A) )).

cnf(maddux2_join_associativity_2,axiom,
    ( join(A,join(B,C)) = join(join(A,B),C) )).

cnf(maddux3_a_kind_of_de_Morgan_3,axiom,
    ( A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) )).

cnf(maddux4_definiton_of_meet_4,axiom,
    ( meet(A,B) = complement(join(complement(A),complement(B))) )).

cnf(composition_associativity_5,axiom,
    ( composition(A,composition(B,C)) = composition(composition(A,B),C) )).

cnf(composition_identity_6,axiom,
    ( composition(A,one) = A )).

cnf(composition_distributivity_7,axiom,
    ( composition(join(A,B),C) = join(composition(A,C),composition(B,C)) )).

cnf(converse_idempotence_8,axiom,
    ( converse(converse(A)) = A )).

cnf(converse_additivity_9,axiom,
    ( converse(join(A,B)) = join(converse(A),converse(B)) )).

cnf(converse_multiplicativity_10,axiom,
    ( converse(composition(A,B)) = composition(converse(B),converse(A)) )).

cnf(converse_cancellativity_11,axiom,
    ( join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) )).

cnf(def_top_12,axiom,
    ( top = join(A,complement(A)) )).

cnf(def_zero_13,axiom,
    ( zero = meet(A,complement(A)) )).

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