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. %------------------------------------------------------------------------------