assign(max_seconds, 120).

%------------------------------------------------------------------------------
% File     : ALG033+1 : TPTP v3.0.1. Released v2.7.0.
% Domain   : General Algebra
% Problem  : Groups 6: REPRESENTATIVES-SATISFY-PROPS-PROBLEM-2
% Version  : Especial.
% English  : 

% Refs     : [Mei03] Meier (2003), Email to G.Sutcliffe
%          : [CM+04] Colton et al. (2004), Automatic Generation of Classifi
% Source   : [Mei03]
% Names    : 

% Status   : Theorem
% Rating   : 0.89 v2.7.0
% Syntax   : Number of formulae    :    5 (   1 unit)
%            Number of atoms       :  592 ( 592 equality)
%            Maximal formula depth :  289 (  70 average)
%            Number of connectives :  603 (  16 ~  ; 215  |; 372  &)
%                                         (   0 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
%            Number of functors    :    9 (   7 constant; 0-2 arity)
%            Number of variables   :    0 (   0 singleton;   0 !;   0 ?)
%            Maximal term depth    :    3 (   2 average)

% Comments : 
%          : tptp2X -f mace4 ALG033+1.p 
%------------------------------------------------------------------------------
%----NOTE WELL: conjecture has been negated
set(prolog_style_variables).
formulas(assumptions).

% ax1, axiom.
    ( -(e0 = e1)
     & -(e0 = e2)
     & -(e0 = e3)
     & -(e0 = e4)
     & -(e0 = e5)
     & -(e1 = e2)
     & -(e1 = e3)
     & -(e1 = e4)
     & -(e1 = e5)
     & -(e2 = e3)
     & -(e2 = e4)
     & -(e2 = e5)
     & -(e3 = e4)
     & -(e3 = e5)
     & -(e4 = e5) ).

% ax2, axiom.
    ( op(e0,e0) = e0
     & op(e0,e1) = e1
     & op(e0,e2) = e2
     & op(e0,e3) = e3
     & op(e0,e4) = e4
     & op(e0,e5) = e5
     & op(e1,e0) = e1
     & op(e1,e1) = e0
     & op(e1,e2) = e3
     & op(e1,e3) = e2
     & op(e1,e4) = e5
     & op(e1,e5) = e4
     & op(e2,e0) = e2
     & op(e2,e1) = e4
     & op(e2,e2) = e0
     & op(e2,e3) = e5
     & op(e2,e4) = e1
     & op(e2,e5) = e3
     & op(e3,e0) = e3
     & op(e3,e1) = e5
     & op(e3,e2) = e1
     & op(e3,e3) = e4
     & op(e3,e4) = e0
     & op(e3,e5) = e2
     & op(e4,e0) = e4
     & op(e4,e1) = e2
     & op(e4,e2) = e5
     & op(e4,e3) = e0
     & op(e4,e4) = e3
     & op(e4,e5) = e1
     & op(e5,e0) = e5
     & op(e5,e1) = e3
     & op(e5,e2) = e4
     & op(e5,e3) = e1
     & op(e5,e4) = e2
     & op(e5,e5) = e0 ).

% ax3, axiom.
    unit = e0.

% ax4, axiom.
    ( inv(e0) = e0
     & inv(e1) = e1
     & inv(e2) = e2
     & inv(e3) = e4
     & inv(e4) = e3
     & inv(e5) = e5 ).

% co1, negated_conjecture.
    -(( -(( op(e0,e0) = op(e0,e0)
           & op(e0,e1) = op(e1,e0)
           & op(e0,e2) = op(e2,e0)
           & op(e0,e3) = op(e3,e0)
           & op(e0,e4) = op(e4,e0)
           & op(e0,e5) = op(e5,e0)
           & op(e1,e0) = op(e0,e1)
           & op(e1,e1) = op(e1,e1)
           & op(e1,e2) = op(e2,e1)
           & op(e1,e3) = op(e3,e1)
           & op(e1,e4) = op(e4,e1)
           & op(e1,e5) = op(e5,e1)
           & op(e2,e0) = op(e0,e2)
           & op(e2,e1) = op(e1,e2)
           & op(e2,e2) = op(e2,e2)
           & op(e2,e3) = op(e3,e2)
           & op(e2,e4) = op(e4,e2)
           & op(e2,e5) = op(e5,e2)
           & op(e3,e0) = op(e0,e3)
           & op(e3,e1) = op(e1,e3)
           & op(e3,e2) = op(e2,e3)
           & op(e3,e3) = op(e3,e3)
           & op(e3,e4) = op(e4,e3)
           & op(e3,e5) = op(e5,e3)
           & op(e4,e0) = op(e0,e4)
           & op(e4,e1) = op(e1,e4)
           & op(e4,e2) = op(e2,e4)
           & op(e4,e3) = op(e3,e4)
           & op(e4,e4) = op(e4,e4)
           & op(e4,e5) = op(e5,e4)
           & op(e5,e0) = op(e0,e5)
           & op(e5,e1) = op(e1,e5)
           & op(e5,e2) = op(e2,e5)
           & op(e5,e3) = op(e3,e5)
           & op(e5,e4) = op(e4,e5)
           & op(e5,e5) = op(e5,e5) ))
       & ( op(e0,e0) = e0
         | op(e0,e0) = e1
         | op(e0,e0) = e2
         | op(e0,e0) = e3
         | op(e0,e0) = e4
         | op(e0,e0) = e5 )
       & ( op(e0,e1) = e0
         | op(e0,e1) = e1
         | op(e0,e1) = e2
         | op(e0,e1) = e3
         | op(e0,e1) = e4
         | op(e0,e1) = e5 )
       & ( op(e0,e2) = e0
         | op(e0,e2) = e1
         | op(e0,e2) = e2
         | op(e0,e2) = e3
         | op(e0,e2) = e4
         | op(e0,e2) = e5 )
       & ( op(e0,e3) = e0
         | op(e0,e3) = e1
         | op(e0,e3) = e2
         | op(e0,e3) = e3
         | op(e0,e3) = e4
         | op(e0,e3) = e5 )
       & ( op(e0,e4) = e0
         | op(e0,e4) = e1
         | op(e0,e4) = e2
         | op(e0,e4) = e3
         | op(e0,e4) = e4
         | op(e0,e4) = e5 )
       & ( op(e0,e5) = e0
         | op(e0,e5) = e1
         | op(e0,e5) = e2
         | op(e0,e5) = e3
         | op(e0,e5) = e4
         | op(e0,e5) = e5 )
       & ( op(e1,e0) = e0
         | op(e1,e0) = e1
         | op(e1,e0) = e2
         | op(e1,e0) = e3
         | op(e1,e0) = e4
         | op(e1,e0) = e5 )
       & ( op(e1,e1) = e0
         | op(e1,e1) = e1
         | op(e1,e1) = e2
         | op(e1,e1) = e3
         | op(e1,e1) = e4
         | op(e1,e1) = e5 )
       & ( op(e1,e2) = e0
         | op(e1,e2) = e1
         | op(e1,e2) = e2
         | op(e1,e2) = e3
         | op(e1,e2) = e4
         | op(e1,e2) = e5 )
       & ( op(e1,e3) = e0
         | op(e1,e3) = e1
         | op(e1,e3) = e2
         | op(e1,e3) = e3
         | op(e1,e3) = e4
         | op(e1,e3) = e5 )
       & ( op(e1,e4) = e0
         | op(e1,e4) = e1
         | op(e1,e4) = e2
         | op(e1,e4) = e3
         | op(e1,e4) = e4
         | op(e1,e4) = e5 )
       & ( op(e1,e5) = e0
         | op(e1,e5) = e1
         | op(e1,e5) = e2
         | op(e1,e5) = e3
         | op(e1,e5) = e4
         | op(e1,e5) = e5 )
       & ( op(e2,e0) = e0
         | op(e2,e0) = e1
         | op(e2,e0) = e2
         | op(e2,e0) = e3
         | op(e2,e0) = e4
         | op(e2,e0) = e5 )
       & ( op(e2,e1) = e0
         | op(e2,e1) = e1
         | op(e2,e1) = e2
         | op(e2,e1) = e3
         | op(e2,e1) = e4
         | op(e2,e1) = e5 )
       & ( op(e2,e2) = e0
         | op(e2,e2) = e1
         | op(e2,e2) = e2
         | op(e2,e2) = e3
         | op(e2,e2) = e4
         | op(e2,e2) = e5 )
       & ( op(e2,e3) = e0
         | op(e2,e3) = e1
         | op(e2,e3) = e2
         | op(e2,e3) = e3
         | op(e2,e3) = e4
         | op(e2,e3) = e5 )
       & ( op(e2,e4) = e0
         | op(e2,e4) = e1
         | op(e2,e4) = e2
         | op(e2,e4) = e3
         | op(e2,e4) = e4
         | op(e2,e4) = e5 )
       & ( op(e2,e5) = e0
         | op(e2,e5) = e1
         | op(e2,e5) = e2
         | op(e2,e5) = e3
         | op(e2,e5) = e4
         | op(e2,e5) = e5 )
       & ( op(e3,e0) = e0
         | op(e3,e0) = e1
         | op(e3,e0) = e2
         | op(e3,e0) = e3
         | op(e3,e0) = e4
         | op(e3,e0) = e5 )
       & ( op(e3,e1) = e0
         | op(e3,e1) = e1
         | op(e3,e1) = e2
         | op(e3,e1) = e3
         | op(e3,e1) = e4
         | op(e3,e1) = e5 )
       & ( op(e3,e2) = e0
         | op(e3,e2) = e1
         | op(e3,e2) = e2
         | op(e3,e2) = e3
         | op(e3,e2) = e4
         | op(e3,e2) = e5 )
       & ( op(e3,e3) = e0
         | op(e3,e3) = e1
         | op(e3,e3) = e2
         | op(e3,e3) = e3
         | op(e3,e3) = e4
         | op(e3,e3) = e5 )
       & ( op(e3,e4) = e0
         | op(e3,e4) = e1
         | op(e3,e4) = e2
         | op(e3,e4) = e3
         | op(e3,e4) = e4
         | op(e3,e4) = e5 )
       & ( op(e3,e5) = e0
         | op(e3,e5) = e1
         | op(e3,e5) = e2
         | op(e3,e5) = e3
         | op(e3,e5) = e4
         | op(e3,e5) = e5 )
       & ( op(e4,e0) = e0
         | op(e4,e0) = e1
         | op(e4,e0) = e2
         | op(e4,e0) = e3
         | op(e4,e0) = e4
         | op(e4,e0) = e5 )
       & ( op(e4,e1) = e0
         | op(e4,e1) = e1
         | op(e4,e1) = e2
         | op(e4,e1) = e3
         | op(e4,e1) = e4
         | op(e4,e1) = e5 )
       & ( op(e4,e2) = e0
         | op(e4,e2) = e1
         | op(e4,e2) = e2
         | op(e4,e2) = e3
         | op(e4,e2) = e4
         | op(e4,e2) = e5 )
       & ( op(e4,e3) = e0
         | op(e4,e3) = e1
         | op(e4,e3) = e2
         | op(e4,e3) = e3
         | op(e4,e3) = e4
         | op(e4,e3) = e5 )
       & ( op(e4,e4) = e0
         | op(e4,e4) = e1
         | op(e4,e4) = e2
         | op(e4,e4) = e3
         | op(e4,e4) = e4
         | op(e4,e4) = e5 )
       & ( op(e4,e5) = e0
         | op(e4,e5) = e1
         | op(e4,e5) = e2
         | op(e4,e5) = e3
         | op(e4,e5) = e4
         | op(e4,e5) = e5 )
       & ( op(e5,e0) = e0
         | op(e5,e0) = e1
         | op(e5,e0) = e2
         | op(e5,e0) = e3
         | op(e5,e0) = e4
         | op(e5,e0) = e5 )
       & ( op(e5,e1) = e0
         | op(e5,e1) = e1
         | op(e5,e1) = e2
         | op(e5,e1) = e3
         | op(e5,e1) = e4
         | op(e5,e1) = e5 )
       & ( op(e5,e2) = e0
         | op(e5,e2) = e1
         | op(e5,e2) = e2
         | op(e5,e2) = e3
         | op(e5,e2) = e4
         | op(e5,e2) = e5 )
       & ( op(e5,e3) = e0
         | op(e5,e3) = e1
         | op(e5,e3) = e2
         | op(e5,e3) = e3
         | op(e5,e3) = e4
         | op(e5,e3) = e5 )
       & ( op(e5,e4) = e0
         | op(e5,e4) = e1
         | op(e5,e4) = e2
         | op(e5,e4) = e3
         | op(e5,e4) = e4
         | op(e5,e4) = e5 )
       & ( op(e5,e5) = e0
         | op(e5,e5) = e1
         | op(e5,e5) = e2
         | op(e5,e5) = e3
         | op(e5,e5) = e4
         | op(e5,e5) = e5 )
       & op(op(e0,e0),e0) = op(e0,op(e0,e0))
       & op(op(e0,e0),e1) = op(e0,op(e0,e1))
       & op(op(e0,e0),e2) = op(e0,op(e0,e2))
       & op(op(e0,e0),e3) = op(e0,op(e0,e3))
       & op(op(e0,e0),e4) = op(e0,op(e0,e4))
       & op(op(e0,e0),e5) = op(e0,op(e0,e5))
       & op(op(e0,e1),e0) = op(e0,op(e1,e0))
       & op(op(e0,e1),e1) = op(e0,op(e1,e1))
       & op(op(e0,e1),e2) = op(e0,op(e1,e2))
       & op(op(e0,e1),e3) = op(e0,op(e1,e3))
       & op(op(e0,e1),e4) = op(e0,op(e1,e4))
       & op(op(e0,e1),e5) = op(e0,op(e1,e5))
       & op(op(e0,e2),e0) = op(e0,op(e2,e0))
       & op(op(e0,e2),e1) = op(e0,op(e2,e1))
       & op(op(e0,e2),e2) = op(e0,op(e2,e2))
       & op(op(e0,e2),e3) = op(e0,op(e2,e3))
       & op(op(e0,e2),e4) = op(e0,op(e2,e4))
       & op(op(e0,e2),e5) = op(e0,op(e2,e5))
       & op(op(e0,e3),e0) = op(e0,op(e3,e0))
       & op(op(e0,e3),e1) = op(e0,op(e3,e1))
       & op(op(e0,e3),e2) = op(e0,op(e3,e2))
       & op(op(e0,e3),e3) = op(e0,op(e3,e3))
       & op(op(e0,e3),e4) = op(e0,op(e3,e4))
       & op(op(e0,e3),e5) = op(e0,op(e3,e5))
       & op(op(e0,e4),e0) = op(e0,op(e4,e0))
       & op(op(e0,e4),e1) = op(e0,op(e4,e1))
       & op(op(e0,e4),e2) = op(e0,op(e4,e2))
       & op(op(e0,e4),e3) = op(e0,op(e4,e3))
       & op(op(e0,e4),e4) = op(e0,op(e4,e4))
       & op(op(e0,e4),e5) = op(e0,op(e4,e5))
       & op(op(e0,e5),e0) = op(e0,op(e5,e0))
       & op(op(e0,e5),e1) = op(e0,op(e5,e1))
       & op(op(e0,e5),e2) = op(e0,op(e5,e2))
       & op(op(e0,e5),e3) = op(e0,op(e5,e3))
       & op(op(e0,e5),e4) = op(e0,op(e5,e4))
       & op(op(e0,e5),e5) = op(e0,op(e5,e5))
       & op(op(e1,e0),e0) = op(e1,op(e0,e0))
       & op(op(e1,e0),e1) = op(e1,op(e0,e1))
       & op(op(e1,e0),e2) = op(e1,op(e0,e2))
       & op(op(e1,e0),e3) = op(e1,op(e0,e3))
       & op(op(e1,e0),e4) = op(e1,op(e0,e4))
       & op(op(e1,e0),e5) = op(e1,op(e0,e5))
       & op(op(e1,e1),e0) = op(e1,op(e1,e0))
       & op(op(e1,e1),e1) = op(e1,op(e1,e1))
       & op(op(e1,e1),e2) = op(e1,op(e1,e2))
       & op(op(e1,e1),e3) = op(e1,op(e1,e3))
       & op(op(e1,e1),e4) = op(e1,op(e1,e4))
       & op(op(e1,e1),e5) = op(e1,op(e1,e5))
       & op(op(e1,e2),e0) = op(e1,op(e2,e0))
       & op(op(e1,e2),e1) = op(e1,op(e2,e1))
       & op(op(e1,e2),e2) = op(e1,op(e2,e2))
       & op(op(e1,e2),e3) = op(e1,op(e2,e3))
       & op(op(e1,e2),e4) = op(e1,op(e2,e4))
       & op(op(e1,e2),e5) = op(e1,op(e2,e5))
       & op(op(e1,e3),e0) = op(e1,op(e3,e0))
       & op(op(e1,e3),e1) = op(e1,op(e3,e1))
       & op(op(e1,e3),e2) = op(e1,op(e3,e2))
       & op(op(e1,e3),e3) = op(e1,op(e3,e3))
       & op(op(e1,e3),e4) = op(e1,op(e3,e4))
       & op(op(e1,e3),e5) = op(e1,op(e3,e5))
       & op(op(e1,e4),e0) = op(e1,op(e4,e0))
       & op(op(e1,e4),e1) = op(e1,op(e4,e1))
       & op(op(e1,e4),e2) = op(e1,op(e4,e2))
       & op(op(e1,e4),e3) = op(e1,op(e4,e3))
       & op(op(e1,e4),e4) = op(e1,op(e4,e4))
       & op(op(e1,e4),e5) = op(e1,op(e4,e5))
       & op(op(e1,e5),e0) = op(e1,op(e5,e0))
       & op(op(e1,e5),e1) = op(e1,op(e5,e1))
       & op(op(e1,e5),e2) = op(e1,op(e5,e2))
       & op(op(e1,e5),e3) = op(e1,op(e5,e3))
       & op(op(e1,e5),e4) = op(e1,op(e5,e4))
       & op(op(e1,e5),e5) = op(e1,op(e5,e5))
       & op(op(e2,e0),e0) = op(e2,op(e0,e0))
       & op(op(e2,e0),e1) = op(e2,op(e0,e1))
       & op(op(e2,e0),e2) = op(e2,op(e0,e2))
       & op(op(e2,e0),e3) = op(e2,op(e0,e3))
       & op(op(e2,e0),e4) = op(e2,op(e0,e4))
       & op(op(e2,e0),e5) = op(e2,op(e0,e5))
       & op(op(e2,e1),e0) = op(e2,op(e1,e0))
       & op(op(e2,e1),e1) = op(e2,op(e1,e1))
       & op(op(e2,e1),e2) = op(e2,op(e1,e2))
       & op(op(e2,e1),e3) = op(e2,op(e1,e3))
       & op(op(e2,e1),e4) = op(e2,op(e1,e4))
       & op(op(e2,e1),e5) = op(e2,op(e1,e5))
       & op(op(e2,e2),e0) = op(e2,op(e2,e0))
       & op(op(e2,e2),e1) = op(e2,op(e2,e1))
       & op(op(e2,e2),e2) = op(e2,op(e2,e2))
       & op(op(e2,e2),e3) = op(e2,op(e2,e3))
       & op(op(e2,e2),e4) = op(e2,op(e2,e4))
       & op(op(e2,e2),e5) = op(e2,op(e2,e5))
       & op(op(e2,e3),e0) = op(e2,op(e3,e0))
       & op(op(e2,e3),e1) = op(e2,op(e3,e1))
       & op(op(e2,e3),e2) = op(e2,op(e3,e2))
       & op(op(e2,e3),e3) = op(e2,op(e3,e3))
       & op(op(e2,e3),e4) = op(e2,op(e3,e4))
       & op(op(e2,e3),e5) = op(e2,op(e3,e5))
       & op(op(e2,e4),e0) = op(e2,op(e4,e0))
       & op(op(e2,e4),e1) = op(e2,op(e4,e1))
       & op(op(e2,e4),e2) = op(e2,op(e4,e2))
       & op(op(e2,e4),e3) = op(e2,op(e4,e3))
       & op(op(e2,e4),e4) = op(e2,op(e4,e4))
       & op(op(e2,e4),e5) = op(e2,op(e4,e5))
       & op(op(e2,e5),e0) = op(e2,op(e5,e0))
       & op(op(e2,e5),e1) = op(e2,op(e5,e1))
       & op(op(e2,e5),e2) = op(e2,op(e5,e2))
       & op(op(e2,e5),e3) = op(e2,op(e5,e3))
       & op(op(e2,e5),e4) = op(e2,op(e5,e4))
       & op(op(e2,e5),e5) = op(e2,op(e5,e5))
       & op(op(e3,e0),e0) = op(e3,op(e0,e0))
       & op(op(e3,e0),e1) = op(e3,op(e0,e1))
       & op(op(e3,e0),e2) = op(e3,op(e0,e2))
       & op(op(e3,e0),e3) = op(e3,op(e0,e3))
       & op(op(e3,e0),e4) = op(e3,op(e0,e4))
       & op(op(e3,e0),e5) = op(e3,op(e0,e5))
       & op(op(e3,e1),e0) = op(e3,op(e1,e0))
       & op(op(e3,e1),e1) = op(e3,op(e1,e1))
       & op(op(e3,e1),e2) = op(e3,op(e1,e2))
       & op(op(e3,e1),e3) = op(e3,op(e1,e3))
       & op(op(e3,e1),e4) = op(e3,op(e1,e4))
       & op(op(e3,e1),e5) = op(e3,op(e1,e5))
       & op(op(e3,e2),e0) = op(e3,op(e2,e0))
       & op(op(e3,e2),e1) = op(e3,op(e2,e1))
       & op(op(e3,e2),e2) = op(e3,op(e2,e2))
       & op(op(e3,e2),e3) = op(e3,op(e2,e3))
       & op(op(e3,e2),e4) = op(e3,op(e2,e4))
       & op(op(e3,e2),e5) = op(e3,op(e2,e5))
       & op(op(e3,e3),e0) = op(e3,op(e3,e0))
       & op(op(e3,e3),e1) = op(e3,op(e3,e1))
       & op(op(e3,e3),e2) = op(e3,op(e3,e2))
       & op(op(e3,e3),e3) = op(e3,op(e3,e3))
       & op(op(e3,e3),e4) = op(e3,op(e3,e4))
       & op(op(e3,e3),e5) = op(e3,op(e3,e5))
       & op(op(e3,e4),e0) = op(e3,op(e4,e0))
       & op(op(e3,e4),e1) = op(e3,op(e4,e1))
       & op(op(e3,e4),e2) = op(e3,op(e4,e2))
       & op(op(e3,e4),e3) = op(e3,op(e4,e3))
       & op(op(e3,e4),e4) = op(e3,op(e4,e4))
       & op(op(e3,e4),e5) = op(e3,op(e4,e5))
       & op(op(e3,e5),e0) = op(e3,op(e5,e0))
       & op(op(e3,e5),e1) = op(e3,op(e5,e1))
       & op(op(e3,e5),e2) = op(e3,op(e5,e2))
       & op(op(e3,e5),e3) = op(e3,op(e5,e3))
       & op(op(e3,e5),e4) = op(e3,op(e5,e4))
       & op(op(e3,e5),e5) = op(e3,op(e5,e5))
       & op(op(e4,e0),e0) = op(e4,op(e0,e0))
       & op(op(e4,e0),e1) = op(e4,op(e0,e1))
       & op(op(e4,e0),e2) = op(e4,op(e0,e2))
       & op(op(e4,e0),e3) = op(e4,op(e0,e3))
       & op(op(e4,e0),e4) = op(e4,op(e0,e4))
       & op(op(e4,e0),e5) = op(e4,op(e0,e5))
       & op(op(e4,e1),e0) = op(e4,op(e1,e0))
       & op(op(e4,e1),e1) = op(e4,op(e1,e1))
       & op(op(e4,e1),e2) = op(e4,op(e1,e2))
       & op(op(e4,e1),e3) = op(e4,op(e1,e3))
       & op(op(e4,e1),e4) = op(e4,op(e1,e4))
       & op(op(e4,e1),e5) = op(e4,op(e1,e5))
       & op(op(e4,e2),e0) = op(e4,op(e2,e0))
       & op(op(e4,e2),e1) = op(e4,op(e2,e1))
       & op(op(e4,e2),e2) = op(e4,op(e2,e2))
       & op(op(e4,e2),e3) = op(e4,op(e2,e3))
       & op(op(e4,e2),e4) = op(e4,op(e2,e4))
       & op(op(e4,e2),e5) = op(e4,op(e2,e5))
       & op(op(e4,e3),e0) = op(e4,op(e3,e0))
       & op(op(e4,e3),e1) = op(e4,op(e3,e1))
       & op(op(e4,e3),e2) = op(e4,op(e3,e2))
       & op(op(e4,e3),e3) = op(e4,op(e3,e3))
       & op(op(e4,e3),e4) = op(e4,op(e3,e4))
       & op(op(e4,e3),e5) = op(e4,op(e3,e5))
       & op(op(e4,e4),e0) = op(e4,op(e4,e0))
       & op(op(e4,e4),e1) = op(e4,op(e4,e1))
       & op(op(e4,e4),e2) = op(e4,op(e4,e2))
       & op(op(e4,e4),e3) = op(e4,op(e4,e3))
       & op(op(e4,e4),e4) = op(e4,op(e4,e4))
       & op(op(e4,e4),e5) = op(e4,op(e4,e5))
       & op(op(e4,e5),e0) = op(e4,op(e5,e0))
       & op(op(e4,e5),e1) = op(e4,op(e5,e1))
       & op(op(e4,e5),e2) = op(e4,op(e5,e2))
       & op(op(e4,e5),e3) = op(e4,op(e5,e3))
       & op(op(e4,e5),e4) = op(e4,op(e5,e4))
       & op(op(e4,e5),e5) = op(e4,op(e5,e5))
       & op(op(e5,e0),e0) = op(e5,op(e0,e0))
       & op(op(e5,e0),e1) = op(e5,op(e0,e1))
       & op(op(e5,e0),e2) = op(e5,op(e0,e2))
       & op(op(e5,e0),e3) = op(e5,op(e0,e3))
       & op(op(e5,e0),e4) = op(e5,op(e0,e4))
       & op(op(e5,e0),e5) = op(e5,op(e0,e5))
       & op(op(e5,e1),e0) = op(e5,op(e1,e0))
       & op(op(e5,e1),e1) = op(e5,op(e1,e1))
       & op(op(e5,e1),e2) = op(e5,op(e1,e2))
       & op(op(e5,e1),e3) = op(e5,op(e1,e3))
       & op(op(e5,e1),e4) = op(e5,op(e1,e4))
       & op(op(e5,e1),e5) = op(e5,op(e1,e5))
       & op(op(e5,e2),e0) = op(e5,op(e2,e0))
       & op(op(e5,e2),e1) = op(e5,op(e2,e1))
       & op(op(e5,e2),e2) = op(e5,op(e2,e2))
       & op(op(e5,e2),e3) = op(e5,op(e2,e3))
       & op(op(e5,e2),e4) = op(e5,op(e2,e4))
       & op(op(e5,e2),e5) = op(e5,op(e2,e5))
       & op(op(e5,e3),e0) = op(e5,op(e3,e0))
       & op(op(e5,e3),e1) = op(e5,op(e3,e1))
       & op(op(e5,e3),e2) = op(e5,op(e3,e2))
       & op(op(e5,e3),e3) = op(e5,op(e3,e3))
       & op(op(e5,e3),e4) = op(e5,op(e3,e4))
       & op(op(e5,e3),e5) = op(e5,op(e3,e5))
       & op(op(e5,e4),e0) = op(e5,op(e4,e0))
       & op(op(e5,e4),e1) = op(e5,op(e4,e1))
       & op(op(e5,e4),e2) = op(e5,op(e4,e2))
       & op(op(e5,e4),e3) = op(e5,op(e4,e3))
       & op(op(e5,e4),e4) = op(e5,op(e4,e4))
       & op(op(e5,e4),e5) = op(e5,op(e4,e5))
       & op(op(e5,e5),e0) = op(e5,op(e5,e0))
       & op(op(e5,e5),e1) = op(e5,op(e5,e1))
       & op(op(e5,e5),e2) = op(e5,op(e5,e2))
       & op(op(e5,e5),e3) = op(e5,op(e5,e3))
       & op(op(e5,e5),e4) = op(e5,op(e5,e4))
       & op(op(e5,e5),e5) = op(e5,op(e5,e5))
       & op(unit,e0) = e0
       & op(e0,unit) = e0
       & op(unit,e1) = e1
       & op(e1,unit) = e1
       & op(unit,e2) = e2
       & op(e2,unit) = e2
       & op(unit,e3) = e3
       & op(e3,unit) = e3
       & op(unit,e4) = e4
       & op(e4,unit) = e4
       & op(unit,e5) = e5
       & op(e5,unit) = e5
       & ( unit = e0
         | unit = e1
         | unit = e2
         | unit = e3
         | unit = e4
         | unit = e5 )
       & op(e0,inv(e0)) = unit
       & op(inv(e0),e0) = unit
       & op(e1,inv(e1)) = unit
       & op(inv(e1),e1) = unit
       & op(e2,inv(e2)) = unit
       & op(inv(e2),e2) = unit
       & op(e3,inv(e3)) = unit
       & op(inv(e3),e3) = unit
       & op(e4,inv(e4)) = unit
       & op(inv(e4),e4) = unit
       & op(e5,inv(e5)) = unit
       & op(inv(e5),e5) = unit
       & ( inv(e0) = e0
         | inv(e0) = e1
         | inv(e0) = e2
         | inv(e0) = e3
         | inv(e0) = e4
         | inv(e0) = e5 )
       & ( inv(e1) = e0
         | inv(e1) = e1
         | inv(e1) = e2
         | inv(e1) = e3
         | inv(e1) = e4
         | inv(e1) = e5 )
       & ( inv(e2) = e0
         | inv(e2) = e1
         | inv(e2) = e2
         | inv(e2) = e3
         | inv(e2) = e4
         | inv(e2) = e5 )
       & ( inv(e3) = e0
         | inv(e3) = e1
         | inv(e3) = e2
         | inv(e3) = e3
         | inv(e3) = e4
         | inv(e3) = e5 )
       & ( inv(e4) = e0
         | inv(e4) = e1
         | inv(e4) = e2
         | inv(e4) = e3
         | inv(e4) = e4
         | inv(e4) = e5 )
       & ( inv(e5) = e0
         | inv(e5) = e1
         | inv(e5) = e2
         | inv(e5) = e3
         | inv(e5) = e4
         | inv(e5) = e5 ) )).
end_of_list.

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