********************  Starting Exceptional Lazard Procedure (logged) *********\
************
####################  Step 1: Construction of a 6-quotient of the rank 3 
3-Engel 5-group of exponent 5.

##### Defining tool functions...
##### ...done.

##### Launching the pq-algorithm...
#I  Lower exponent-5 central series for [grp]
#I  Group: [grp] to lower exponent-5 central class 1 has order 5^3
#I  Class 1 with 3 generators.
#I  Group: [grp] to lower exponent-5 central class 2 has order 5^9
#I  Class 2 with 6 generators.
#I  Group: [grp] to lower exponent-5 central class 3 has order 5^17
#I  Class 3 with 14 generators.
#I  Group: [grp] to lower exponent-5 central class 4 has order 5^35
#I  Class 4 with 17 generators.
#I  Group: [grp] to lower exponent-5 central class 5 has order 5^44
#I  Class 5 with 20 generators.
#I  Group: [grp] to lower exponent-5 central class 6 has order 5^52
#I  Class 5 with 20 generators.
##### ...done.
##### Nilpotency class of the 3-generated group = 5.

####################  End of Step 1.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Runtime : 0 day(s), 0 hour(s), 0 minute(s), 7 seconde(s).
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
####################  Step 2: Construction of the functions Su and Br.

####################  End of Step 2.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Runtime : 0 day(s), 0 hour(s), 0 minute(s), 7 seconde(s).
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
####################  Step 3: Checking Properties of Su and Br.

##### Checking that Su...
1. is commutative:
+++ true +++
2. is associative:
+++ true +++
3. Identity is neutral:
+++ true +++
4. has exponent: 5:
+++ true +++
##### Conclusions for Su: [ true, true, true, true 
 ] (The binary function defines an elementary abelian group of exponent: 5)

##### Checking that Br...
1. is antisymmetric:
+++ true +++
2. is left-bilinear:
+++ true +++
3. is right-bilinear:
+++ true +++
4. satisfies Jacobi:
+++ true +++
##### Conclusions for Br: [ true, true, true, true 
 ] (Su and Br define a Lie algebra structure.)



##### Checking brace structure...
+++ false +++
+++ false +++
##### Conclusions for brace: [ false, false ]

##### Checking associativity formula [y,z]^n-1 = y^n-1z^n-1...
[y,z]^n-1 is nonzero.
+++ false +++
+++ true +++
##### Conclusions for associativity formula [y,z]^n-1 = y^n-1z^n-1, [y,z]^n-1 \
= - y^n-1z^n-1: [ false, true ]

##### Checking commutativity formula x^n-1y^n-1 = y^n-1x^n-1...
y^n-1z^n-1 is nonzero.
+++ true +++
+++ false +++
##### Conclusions for commutativity formula x^n-1y^n-1 = y^n-1z^n-1, x^n-1y^n-\
1 = - y^n-1z^n-1: [ true, false ]

####################  End of Step 3.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Runtime : 0 day(s), 0 hour(s), 0 minute(s), 7 seconde(s).
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
####################  Step 4: Checking Properties of the BCH formula from Pr a\
nd Br.

##### Definition of the functions twos sum...

##### Checking that PrLeft...
1. coincides with product:
+++ true +++
2. is associative:
+++ true +++
3. Identity is neutral:
+++ true +++
4. has exponent: 5:
+++ true +++
##### Conclusions for PrLeft: [ true, true, true, true 
 ] (The BCH applied with Pr and Br coincides with the product, for left-normed\
 iterations of Su.)

##### Checking that PrRight...
1. coincides with product:
+++ false +++
2. is associative:
+++ false +++
3. Identity is neutral:
+++ false +++
4. has exponent: 5:
+++ true +++
##### Conclusions for PrRight: [ false, false, false, true ]

####################  End of Step 4.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Runtime : 0 day(s), 0 hour(s), 0 minute(s), 7 seconde(s).
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

********************  End of Engel procedure (logged) *********************