Via this web page you have access to supplementary materials for the paper

**The crucial Knuth-Bendix computation: proving T
is nilpotent.**

In a directory which includes the three files final.rl1, final.sys and final.sb1, run

input final summary kb 10 2 10 10 summary add_engel 4 2 0 5 10 10 summary kb 10 1 10 10 summary rewrite_words none names subword x11x11 [x10,x1,x1] [x10,x1,x2] [x10,x1,x3] [x10,x3] [x9,x3] [x7,x2] [x6,x2] [x4,x2] @ quitThe output of this run gives us the following relations: x11x11 = [x10,x1,x2] = [x10,x1,x3] = [x10,x3] = 1; [x10,x1,x1] = x11; [x9,x3] = x1x10X1X10; [x7,x2] = x10x10; [x6,x2] = x3x9X3; and [x4,x2] = x8x10. From these we can deduce that

Alternatively, we can observe the following relations: [x11,x1] =
[x11,x2] = [x11,x3] = [x10,x1,x2] = [x10,x1,x3] = [x10,x3] = 1;
[x10,x1,x1] = x11; [x9,x3] = x1x10X1X10; [x7,x2] = x10x10; [x6,x2] =
x3x9X3; and [x4,x2] = x8x10.
Adding these relations to *T* we can obtain a confluent rewriting
system by now doing a Knuth-Bendix computation with a wreath product ordering.
In a directory which includes the three files
check.rl1,
check.sys and
check.sb1,
run `rkbp` with the following input commands:

input check summary kb 10 -1 4 50 summary add_engel 4 3 0 5 4 50 summaryThis shows that