We consider two TRSs R and S where R contains the rules
| h(f'(f'(f'(h(c,h(b,c))))),h(f'(f'(b)),b)) | → | f'(h(b,f'(a))) | (1) |
| f'(c) | → | b | (2) |
and S contains the following rules:
| a | → | b | (3) |
| f(x,a) | → | b | (4) |
| f(b,b) | → | b | (5) |
The underlying signature is as follows:
{a/0, b/0, c/0, f/2, h/2, f'/1}