We consider the TRS containing the following rules:
| a1 | → | b1 | (1) |
| a1 | → | c1 | (2) |
| b1 | → | b2 | (3) |
| c1 | → | c2 | (4) |
| a2 | → | b2 | (5) |
| a2 | → | c2 | (6) |
| b2 | → | b3 | (7) |
| c2 | → | c3 | (8) |
| a3 | → | b3 | (9) |
| a3 | → | c3 | (10) |
| b3 | → | b4 | (11) |
| c3 | → | c4 | (12) |
| a4 | → | b4 | (13) |
| a4 | → | c4 | (14) |
| b4 | → | b5 | (15) |
| c4 | → | c5 | (16) |
| a5 | → | b5 | (17) |
| a5 | → | c5 | (18) |
| b5 | → | b6 | (19) |
| c5 | → | c6 | (20) |
| a6 | → | b6 | (21) |
| a6 | → | c6 | (22) |
| b6 | → | b7 | (23) |
| c6 | → | c7 | (24) |
| a7 | → | b7 | (25) |
| a7 | → | c7 | (26) |
| b7 | → | b8 | (27) |
| c7 | → | c8 | (28) |
| a8 | → | b8 | (29) |
| a8 | → | c8 | (30) |
| b8 | → | b9 | (31) |
| c8 | → | c9 | (32) |
| a9 | → | b9 | (33) |
| a9 | → | c9 | (34) |
| b9 | → | b10 | (35) |
| c9 | → | c10 | (36) |
| a10 | → | b11 | (37) |
| b10 | → | b11 | (38) |
| c10 | → | b11 | (39) |
The underlying signature is as follows:
{a1/0, b1/0, c1/0, b2/0, c2/0, a2/0, b3/0, c3/0, a3/0, b4/0, c4/0, a4/0, b5/0, c5/0, a5/0, b6/0, c6/0, a6/0, b7/0, c7/0, a7/0, b8/0, c8/0, a8/0, b9/0, c9/0, a9/0, b10/0, c10/0, a10/0, b11/0}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| c10 | → | b11 | (39) |
| b10 | → | b11 | (38) |
| a10 | → | b11 | (37) |
| c9 | → | c10 | (36) |
| b9 | → | b10 | (35) |
| a9 | → | c9 | (34) |
| a9 | → | b9 | (33) |
| c8 | → | c9 | (32) |
| b8 | → | b9 | (31) |
| a8 | → | c8 | (30) |
| a8 | → | b8 | (29) |
| c7 | → | c8 | (28) |
| b7 | → | b8 | (27) |
| a7 | → | c7 | (26) |
| a7 | → | b7 | (25) |
| c6 | → | c7 | (24) |
| b6 | → | b7 | (23) |
| a6 | → | c6 | (22) |
| a6 | → | b6 | (21) |
| c5 | → | c6 | (20) |
| b5 | → | b6 | (19) |
| a5 | → | c5 | (18) |
| a5 | → | b5 | (17) |
| c4 | → | c5 | (16) |
| b4 | → | b5 | (15) |
| a4 | → | c4 | (14) |
| a4 | → | b4 | (13) |
| c3 | → | c4 | (12) |
| b3 | → | b4 | (11) |
| a3 | → | c3 | (10) |
| a3 | → | b3 | (9) |
| c2 | → | c3 | (8) |
| b2 | → | b3 | (7) |
| a2 | → | c2 | (6) |
| a2 | → | b2 | (5) |
| c1 | → | c2 | (4) |
| b1 | → | b2 | (3) |
| a1 | → | c1 | (2) |
| a1 | → | b1 | (1) |
| b1 | → | b11 | (40) |
| c1 | → | b11 | (41) |
| b2 | → | b11 | (42) |
| c2 | → | b11 | (43) |
| b3 | → | b11 | (44) |
| c3 | → | b11 | (45) |
| b4 | → | b11 | (46) |
| c4 | → | b11 | (47) |
| b5 | → | b11 | (48) |
| c5 | → | b11 | (49) |
| b6 | → | b11 | (50) |
| c6 | → | b11 | (51) |
| b7 | → | b11 | (52) |
| c7 | → | b11 | (53) |
| b8 | → | b11 | (54) |
| c8 | → | b11 | (55) |
| b9 | → | b11 | (56) |
| c9 | → | b11 | (57) |
All redundant rules that were added or removed can be simulated in 10 steps .