Certification Problem

Input (TPDB SRS_Relative/Waldmann_19/random-38)

The relative rewrite relation R/S is considered where R is the following TRS

a(c(b(x1))) → b(b(a(x1))) (1)
a(c(b(x1))) → a(c(c(x1))) (2)
b(b(b(x1))) → a(a(c(x1))) (3)
c(a(c(x1))) → b(b(b(x1))) (4)

and S is the following TRS.

b(a(b(x1))) → b(a(b(x1))) (5)
b(a(a(x1))) → b(a(b(x1))) (6)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{c(☐), b(☐), a(☐)}

We obtain the transformed TRS
c(a(c(b(x1)))) → c(b(b(a(x1)))) (7)
c(a(c(b(x1)))) → c(a(c(c(x1)))) (8)
c(b(b(b(x1)))) → c(a(a(c(x1)))) (9)
c(c(a(c(x1)))) → c(b(b(b(x1)))) (10)
c(b(a(a(x1)))) → c(b(a(b(x1)))) (11)
b(a(c(b(x1)))) → b(b(b(a(x1)))) (12)
b(a(c(b(x1)))) → b(a(c(c(x1)))) (13)
b(b(b(b(x1)))) → b(a(a(c(x1)))) (14)
b(c(a(c(x1)))) → b(b(b(b(x1)))) (15)
b(b(a(a(x1)))) → b(b(a(b(x1)))) (16)
a(a(c(b(x1)))) → a(b(b(a(x1)))) (17)
a(a(c(b(x1)))) → a(a(c(c(x1)))) (18)
a(b(b(b(x1)))) → a(a(a(c(x1)))) (19)
a(c(a(c(x1)))) → a(b(b(b(x1)))) (20)
a(b(a(a(x1)))) → a(b(a(b(x1)))) (21)

1.1 Closure Under Flat Contexts

Using the flat contexts

{c(☐), b(☐), a(☐)}

We obtain the transformed TRS
c(c(a(c(b(x1))))) → c(c(b(b(a(x1))))) (22)
c(c(a(c(b(x1))))) → c(c(a(c(c(x1))))) (23)
c(c(b(b(b(x1))))) → c(c(a(a(c(x1))))) (24)
c(c(c(a(c(x1))))) → c(c(b(b(b(x1))))) (25)
c(c(b(a(a(x1))))) → c(c(b(a(b(x1))))) (26)
c(b(a(c(b(x1))))) → c(b(b(b(a(x1))))) (27)
c(b(a(c(b(x1))))) → c(b(a(c(c(x1))))) (28)
c(b(b(b(b(x1))))) → c(b(a(a(c(x1))))) (29)
c(b(c(a(c(x1))))) → c(b(b(b(b(x1))))) (30)
c(b(b(a(a(x1))))) → c(b(b(a(b(x1))))) (31)
c(a(a(c(b(x1))))) → c(a(b(b(a(x1))))) (32)
c(a(a(c(b(x1))))) → c(a(a(c(c(x1))))) (33)
c(a(b(b(b(x1))))) → c(a(a(a(c(x1))))) (34)
c(a(c(a(c(x1))))) → c(a(b(b(b(x1))))) (35)
c(a(b(a(a(x1))))) → c(a(b(a(b(x1))))) (36)
b(c(a(c(b(x1))))) → b(c(b(b(a(x1))))) (37)
b(c(a(c(b(x1))))) → b(c(a(c(c(x1))))) (38)
b(c(b(b(b(x1))))) → b(c(a(a(c(x1))))) (39)
b(c(c(a(c(x1))))) → b(c(b(b(b(x1))))) (40)
b(c(b(a(a(x1))))) → b(c(b(a(b(x1))))) (41)
b(b(a(c(b(x1))))) → b(b(b(b(a(x1))))) (42)
b(b(a(c(b(x1))))) → b(b(a(c(c(x1))))) (43)
b(b(b(b(b(x1))))) → b(b(a(a(c(x1))))) (44)
b(b(c(a(c(x1))))) → b(b(b(b(b(x1))))) (45)
b(b(b(a(a(x1))))) → b(b(b(a(b(x1))))) (46)
b(a(a(c(b(x1))))) → b(a(b(b(a(x1))))) (47)
b(a(a(c(b(x1))))) → b(a(a(c(c(x1))))) (48)
b(a(b(b(b(x1))))) → b(a(a(a(c(x1))))) (49)
b(a(c(a(c(x1))))) → b(a(b(b(b(x1))))) (50)
b(a(b(a(a(x1))))) → b(a(b(a(b(x1))))) (51)
a(c(a(c(b(x1))))) → a(c(b(b(a(x1))))) (52)
a(c(a(c(b(x1))))) → a(c(a(c(c(x1))))) (53)
a(c(b(b(b(x1))))) → a(c(a(a(c(x1))))) (54)
a(c(c(a(c(x1))))) → a(c(b(b(b(x1))))) (55)
a(c(b(a(a(x1))))) → a(c(b(a(b(x1))))) (56)
a(b(a(c(b(x1))))) → a(b(b(b(a(x1))))) (57)
a(b(a(c(b(x1))))) → a(b(a(c(c(x1))))) (58)
a(b(b(b(b(x1))))) → a(b(a(a(c(x1))))) (59)
a(b(c(a(c(x1))))) → a(b(b(b(b(x1))))) (60)
a(b(b(a(a(x1))))) → a(b(b(a(b(x1))))) (61)
a(a(a(c(b(x1))))) → a(a(b(b(a(x1))))) (62)
a(a(a(c(b(x1))))) → a(a(a(c(c(x1))))) (63)
a(a(b(b(b(x1))))) → a(a(a(a(c(x1))))) (64)
a(a(c(a(c(x1))))) → a(a(b(b(b(x1))))) (65)
a(a(b(a(a(x1))))) → a(a(b(a(b(x1))))) (66)

1.1.1 Closure Under Flat Contexts

Using the flat contexts

{c(☐), b(☐), a(☐)}

We obtain the transformed TRS

There are 135 ruless (increase limit for explicit display).

1.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

As carrier we take the set {0,...,26}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 27):

[c(x1)] = 3x1 + 0
[b(x1)] = 3x1 + 1
[a(x1)] = 3x1 + 2

We obtain the labeled TRS

There are 3645 ruless (increase limit for explicit display).

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[c0(x1)] = x1 +
1076/3
[c9(x1)] = x1 +
1076/3
[c18(x1)] = x1 +
1076/3
[c3(x1)] = x1 +
103/3
[c12(x1)] = x1 +
103/3
[c21(x1)] = x1 +
103/3
[c6(x1)] = x1 +
988/3
[c15(x1)] = x1 +
2
[c24(x1)] = x1 +
103/3
[c1(x1)] = x1 +
1270/3
[c10(x1)] = x1 +
973/3
[c19(x1)] = x1 +
1270/3
[c4(x1)] = x1 +
1270/3
[c13(x1)] = x1 +
988/3
[c22(x1)] = x1 +
99
[c7(x1)] = x1 +
973/3
[c16(x1)] = x1 +
5
[c25(x1)] = x1 +
5
[c2(x1)] = x1 +
973/3
[c11(x1)] = x1 +
988/3
[c20(x1)] = x1 +
973/3
[c5(x1)] = x1 +
0
[c14(x1)] = x1 +
0
[c23(x1)] = x1 +
2
[c8(x1)] = x1 +
99
[c17(x1)] = x1 +
103/3
[c26(x1)] = x1 +
99
[b0(x1)] = x1 +
973/3
[b9(x1)] = x1 +
973/3
[b18(x1)] = x1 +
973/3
[b3(x1)] = x1 +
337
[b12(x1)] = x1 +
337
[b21(x1)] = x1 +
337
[b6(x1)] = x1 +
988/3
[b15(x1)] = x1 +
0
[b24(x1)] = x1 +
0
[b1(x1)] = x1 +
973/3
[b10(x1)] = x1 +
38/3
[b19(x1)] = x1 +
973/3
[b4(x1)] = x1 +
973/3
[b13(x1)] = x1 +
983/3
[b22(x1)] = x1 +
5
[b7(x1)] = x1 +
973/3
[b16(x1)] = x1 +
5
[b25(x1)] = x1 +
5
[b2(x1)] = x1 +
973/3
[b11(x1)] = x1 +
988/3
[b20(x1)] = x1 +
976/3
[b5(x1)] = x1 +
38/3
[b14(x1)] = x1 +
5
[b23(x1)] = x1 +
5
[b8(x1)] = x1 +
1076/3
[b17(x1)] = x1 +
988/3
[b26(x1)] = x1 +
973/3
[a0(x1)] = x1 +
1076/3
[a9(x1)] = x1 +
1076/3
[a18(x1)] = x1 +
988/3
[a3(x1)] = x1 +
973/3
[a12(x1)] = x1 +
988/3
[a21(x1)] = x1 +
988/3
[a6(x1)] = x1 +
973/3
[a15(x1)] = x1 +
0
[a24(x1)] = x1 +
103/3
[a1(x1)] = x1 +
337
[a10(x1)] = x1 +
99
[a19(x1)] = x1 +
337
[a4(x1)] = x1 +
976/3
[a13(x1)] = x1 +
326
[a22(x1)] = x1 +
10/3
[a7(x1)] = x1 +
0
[a16(x1)] = x1 +
0
[a25(x1)] = x1 +
0
[a2(x1)] = x1 +
0
[a11(x1)] = x1 +
5
[a20(x1)] = x1 +
2
[a5(x1)] = x1 +
0
[a14(x1)] = x1 +
10/3
[a23(x1)] = x1 +
10/3
[a8(x1)] = x1 +
5
[a17(x1)] = x1 +
0
[a26(x1)] = x1 +
99
all of the following rules can be deleted.

There are 3429 ruless (increase limit for explicit display).

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[c9(x1)] =
2
· x1 +
1
[c18(x1)] =
2
· x1 +
1
[c12(x1)] =
2
· x1 +
1
[c21(x1)] =
1
· x1 +
1
[c6(x1)] =
2
· x1 +
0
[c15(x1)] =
2
· x1 +
1
[c24(x1)] =
2
· x1 +
1
[c10(x1)] =
2
· x1 +
1
[c19(x1)] =
2
· x1 +
1
[c13(x1)] =
2
· x1 +
0
[c22(x1)] =
1
· x1 +
1
[c7(x1)] =
2
· x1 +
0
[c16(x1)] =
2
· x1 +
1
[c25(x1)] =
2
· x1 +
1
[c2(x1)] =
2
· x1 +
0
[c11(x1)] =
2
· x1 +
0
[c20(x1)] =
2
· x1 +
1
[c14(x1)] =
2
· x1 +
1
[c23(x1)] =
1
· x1 +
1
[c8(x1)] =
1
· x1 +
1
[c17(x1)] =
2
· x1 +
1
[c26(x1)] =
1
· x1 +
1
[b9(x1)] =
2
· x1 +
1
[b18(x1)] =
2
· x1 +
1
[b12(x1)] =
2
· x1 +
1
[b21(x1)] =
2
· x1 +
1
[b6(x1)] =
2
· x1 +
0
[b15(x1)] =
2
· x1 +
1
[b24(x1)] =
2
· x1 +
1
[b10(x1)] =
2
· x1 +
1
[b19(x1)] =
2
· x1 +
0
[b4(x1)] =
2
· x1 +
0
[b13(x1)] =
2
· x1 +
0
[b22(x1)] =
2
· x1 +
1
[b7(x1)] =
2
· x1 +
0
[b16(x1)] =
2
· x1 +
1
[b25(x1)] =
2
· x1 +
1
[b2(x1)] =
2
· x1 +
0
[b11(x1)] =
2
· x1 +
0
[b20(x1)] =
2
· x1 +
1
[b14(x1)] =
1
· x1 +
1
[b23(x1)] =
2
· x1 +
1
[b8(x1)] =
1
· x1 +
1
[b17(x1)] =
2
· x1 +
0
[b26(x1)] =
2
· x1 +
0
[a9(x1)] =
1
· x1 +
1
[a18(x1)] =
2
· x1 +
0
[a12(x1)] =
2
· x1 +
0
[a21(x1)] =
2
· x1 +
0
[a6(x1)] =
2
· x1 +
1
[a15(x1)] =
2
· x1 +
1
[a24(x1)] =
2
· x1 +
1
[a10(x1)] =
2
· x1 +
1
[a19(x1)] =
2
· x1 +
1
[a13(x1)] =
2
· x1 +
1
[a22(x1)] =
2
· x1 +
1
[a7(x1)] =
1
· x1 +
1
[a16(x1)] =
2
· x1 +
1
[a25(x1)] =
2
· x1 +
1
[a2(x1)] =
1
· x1 +
1
[a11(x1)] =
1
· x1 +
1
[a20(x1)] =
2
· x1 +
1
[a14(x1)] =
1
· x1 +
1
[a23(x1)] =
2
· x1 +
0
[a8(x1)] =
2
· x1 +
0
[a17(x1)] =
1
· x1 +
1
[a26(x1)] =
1
· x1 +
1
all of the following rules can be deleted.

There are 127 ruless (increase limit for explicit display).

1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[c9(x1)] = x1 +
0
[c18(x1)] = x1 +
0
[c12(x1)] = x1 +
0
[c21(x1)] = x1 +
0
[c6(x1)] = x1 +
7/3
[c15(x1)] = x1 +
0
[c24(x1)] = x1 +
0
[c10(x1)] = x1 +
0
[c19(x1)] = x1 +
0
[c13(x1)] = x1 +
1
[c22(x1)] = x1 +
0
[c7(x1)] = x1 +
9/2
[c16(x1)] = x1 +
0
[c25(x1)] = x1 +
9/2
[c2(x1)] = x1 +
7/3
[c11(x1)] = x1 +
1
[c20(x1)] = x1 +
0
[c14(x1)] = x1 +
0
[c23(x1)] = x1 +
0
[c8(x1)] = x1 +
0
[c17(x1)] = x1 +
0
[c26(x1)] = x1 +
0
[b9(x1)] = x1 +
0
[b18(x1)] = x1 +
0
[b12(x1)] = x1 +
0
[b21(x1)] = x1 +
0
[b6(x1)] = x1 +
1
[b15(x1)] = x1 +
0
[b24(x1)] = x1 +
0
[b10(x1)] = x1 +
0
[b19(x1)] = x1 +
1
[b4(x1)] = x1 +
1
[b13(x1)] = x1 +
0
[b22(x1)] = x1 +
0
[b7(x1)] = x1 +
0
[b16(x1)] = x1 +
0
[b25(x1)] = x1 +
9/2
[b2(x1)] = x1 +
7/3
[b11(x1)] = x1 +
0
[b20(x1)] = x1 +
0
[b14(x1)] = x1 +
0
[b23(x1)] = x1 +
0
[b8(x1)] = x1 +
0
[b17(x1)] = x1 +
9/2
[b26(x1)] = x1 +
0
[a9(x1)] = x1 +
0
[a18(x1)] = x1 +
7/3
[a12(x1)] = x1 +
1
[a21(x1)] = x1 +
9/2
[a6(x1)] = x1 +
0
[a15(x1)] = x1 +
0
[a24(x1)] = x1 +
0
[a10(x1)] = x1 +
0
[a19(x1)] = x1 +
0
[a13(x1)] = x1 +
0
[a22(x1)] = x1 +
9/2
[a7(x1)] = x1 +
0
[a16(x1)] = x1 +
0
[a25(x1)] = x1 +
9/2
[a2(x1)] = x1 +
7/3
[a11(x1)] = x1 +
0
[a20(x1)] = x1 +
0
[a14(x1)] = x1 +
9/2
[a23(x1)] = x1 +
0
[a8(x1)] = x1 +
0
[a17(x1)] = x1 +
0
[a26(x1)] = x1 +
0
all of the following rules can be deleted.
a26(a8(a11(a21(c7(b2(x1)))))) → a26(a8(a2(a18(c6(c2(x1)))))) (935)
a26(a8(a11(a21(c7(b11(x1)))))) → a26(a8(a2(a18(c6(c11(x1)))))) (936)
a20(a6(c11(a21(c7(b2(x1)))))) → a20(a6(c2(a18(c6(c2(x1)))))) (962)
a20(a6(c11(a21(c7(b11(x1)))))) → a20(a6(c2(a18(c6(c11(x1)))))) (963)
a23(a7(b11(a21(c7(b2(x1)))))) → a23(a7(b2(a18(c6(c2(x1)))))) (989)
a23(a7(b11(a21(c7(b11(x1)))))) → a23(a7(b2(a18(c6(c11(x1)))))) (990)
a24(c8(a11(a21(c7(b2(x1)))))) → a24(c8(a2(a18(c6(c2(x1)))))) (1016)
a24(c8(a11(a21(c7(b11(x1)))))) → a24(c8(a2(a18(c6(c11(x1)))))) (1017)
a18(c6(c11(a21(c7(b2(x1)))))) → a18(c6(c2(a18(c6(c2(x1)))))) (1043)
a18(c6(c11(a21(c7(b11(x1)))))) → a18(c6(c2(a18(c6(c11(x1)))))) (1044)
a21(c7(b11(a21(c7(b2(x1)))))) → a21(c7(b2(a18(c6(c2(x1)))))) (1070)
a21(c7(b11(a21(c7(b11(x1)))))) → a21(c7(b2(a18(c6(c11(x1)))))) (1071)
a25(b8(a11(a21(c7(b2(x1)))))) → a25(b8(a2(a18(c6(c2(x1)))))) (1097)
a25(b8(a11(a21(c7(b11(x1)))))) → a25(b8(a2(a18(c6(c11(x1)))))) (1098)
a19(b6(c11(a21(c7(b2(x1)))))) → a19(b6(c2(a18(c6(c2(x1)))))) (1124)
a19(b6(c11(a21(c7(b11(x1)))))) → a19(b6(c2(a18(c6(c11(x1)))))) (1125)
a22(b7(b11(a21(c7(b2(x1)))))) → a22(b7(b2(a18(c6(c2(x1)))))) (1151)
a22(b7(b11(a21(c7(b11(x1)))))) → a22(b7(b2(a18(c6(c11(x1)))))) (1152)
c26(a8(a11(a21(c7(b2(x1)))))) → c26(a8(a2(a18(c6(c2(x1)))))) (1178)
c26(a8(a11(a21(c7(b11(x1)))))) → c26(a8(a2(a18(c6(c11(x1)))))) (1179)
c20(a6(c11(a21(c7(b2(x1)))))) → c20(a6(c2(a18(c6(c2(x1)))))) (1205)
c20(a6(c11(a21(c7(b11(x1)))))) → c20(a6(c2(a18(c6(c11(x1)))))) (1206)
c23(a7(b11(a21(c7(b2(x1)))))) → c23(a7(b2(a18(c6(c2(x1)))))) (1232)
c23(a7(b11(a21(c7(b11(x1)))))) → c23(a7(b2(a18(c6(c11(x1)))))) (1233)
c24(c8(a11(a21(c7(b2(x1)))))) → c24(c8(a2(a18(c6(c2(x1)))))) (1259)
c24(c8(a11(a21(c7(b11(x1)))))) → c24(c8(a2(a18(c6(c11(x1)))))) (1260)
c18(c6(c11(a21(c7(b2(x1)))))) → c18(c6(c2(a18(c6(c2(x1)))))) (1286)
c18(c6(c11(a21(c7(b11(x1)))))) → c18(c6(c2(a18(c6(c11(x1)))))) (1287)
c21(c7(b11(a21(c7(b2(x1)))))) → c21(c7(b2(a18(c6(c2(x1)))))) (1313)
c21(c7(b11(a21(c7(b11(x1)))))) → c21(c7(b2(a18(c6(c11(x1)))))) (1314)
c25(b8(a11(a21(c7(b2(x1)))))) → c25(b8(a2(a18(c6(c2(x1)))))) (1340)
c25(b8(a11(a21(c7(b11(x1)))))) → c25(b8(a2(a18(c6(c11(x1)))))) (1341)
c19(b6(c11(a21(c7(b2(x1)))))) → c19(b6(c2(a18(c6(c2(x1)))))) (1367)
c19(b6(c11(a21(c7(b11(x1)))))) → c19(b6(c2(a18(c6(c11(x1)))))) (1368)
c22(b7(b11(a21(c7(b2(x1)))))) → c22(b7(b2(a18(c6(c2(x1)))))) (1394)
c22(b7(b11(a21(c7(b11(x1)))))) → c22(b7(b2(a18(c6(c11(x1)))))) (1395)
b26(a8(a11(a21(c7(b2(x1)))))) → b26(a8(a2(a18(c6(c2(x1)))))) (1421)
b26(a8(a11(a21(c7(b11(x1)))))) → b26(a8(a2(a18(c6(c11(x1)))))) (1422)
b20(a6(c11(a21(c7(b2(x1)))))) → b20(a6(c2(a18(c6(c2(x1)))))) (1448)
b20(a6(c11(a21(c7(b11(x1)))))) → b20(a6(c2(a18(c6(c11(x1)))))) (1449)
b23(a7(b11(a21(c7(b2(x1)))))) → b23(a7(b2(a18(c6(c2(x1)))))) (1475)
b23(a7(b11(a21(c7(b11(x1)))))) → b23(a7(b2(a18(c6(c11(x1)))))) (1476)
b24(c8(a11(a21(c7(b2(x1)))))) → b24(c8(a2(a18(c6(c2(x1)))))) (1502)
b24(c8(a11(a21(c7(b11(x1)))))) → b24(c8(a2(a18(c6(c11(x1)))))) (1503)
b18(c6(c11(a21(c7(b2(x1)))))) → b18(c6(c2(a18(c6(c2(x1)))))) (1529)
b18(c6(c11(a21(c7(b11(x1)))))) → b18(c6(c2(a18(c6(c11(x1)))))) (1530)
b21(c7(b11(a21(c7(b2(x1)))))) → b21(c7(b2(a18(c6(c2(x1)))))) (1556)
b21(c7(b11(a21(c7(b11(x1)))))) → b21(c7(b2(a18(c6(c11(x1)))))) (1557)
b25(b8(a11(a21(c7(b2(x1)))))) → b25(b8(a2(a18(c6(c2(x1)))))) (1583)
b25(b8(a11(a21(c7(b11(x1)))))) → b25(b8(a2(a18(c6(c11(x1)))))) (1584)
b19(b6(c11(a21(c7(b2(x1)))))) → b19(b6(c2(a18(c6(c2(x1)))))) (1610)
b19(b6(c11(a21(c7(b11(x1)))))) → b19(b6(c2(a18(c6(c11(x1)))))) (1611)
b22(b7(b11(a21(c7(b2(x1)))))) → b22(b7(b2(a18(c6(c2(x1)))))) (1637)
b22(b7(b11(a21(c7(b11(x1)))))) → b22(b7(b2(a18(c6(c11(x1)))))) (1638)
a2(a18(c6(c2(a18(c6(x1)))))) → a11(a12(c13(b4(b19(b6(x1)))))) (2426)
a2(a18(c6(c11(a12(c13(x1)))))) → a11(a12(c13(b13(b13(b13(x1)))))) (2442)
c2(a18(c6(c2(a18(c6(x1)))))) → c11(a12(c13(b4(b19(b6(x1)))))) (2669)
c2(a18(c6(c11(a12(c13(x1)))))) → c11(a12(c13(b13(b13(b13(x1)))))) (2685)
b2(a18(c6(c2(a18(c6(x1)))))) → b11(a12(c13(b4(b19(b6(x1)))))) (2912)
b2(a18(c6(c11(a12(c13(x1)))))) → b11(a12(c13(b13(b13(b13(x1)))))) (2928)
b4(b19(b6(c2(a18(c6(x1)))))) → b13(b13(b13(b4(b19(b6(x1)))))) (3101)
b4(b19(b6(c11(a12(c13(x1)))))) → b13(b13(b13(b13(b13(b13(x1)))))) (3117)
a17(a23(a25(b17(a14(a22(x1)))))) → a17(a23(a16(b14(a13(b22(x1)))))) (3142)
a11(a21(c25(b17(a14(a22(x1)))))) → a11(a21(c16(b14(a13(b22(x1)))))) (3169)
a14(a22(b25(b17(a14(a22(x1)))))) → a14(a22(b16(b14(a13(b22(x1)))))) (3196)
a15(c23(a25(b17(a14(a22(x1)))))) → a15(c23(a16(b14(a13(b22(x1)))))) (3223)
a9(c21(c25(b17(a14(a22(x1)))))) → a9(c21(c16(b14(a13(b22(x1)))))) (3250)
a12(c22(b25(b17(a14(a22(x1)))))) → a12(c22(b16(b14(a13(b22(x1)))))) (3277)
a16(b23(a25(b17(a14(a22(x1)))))) → a16(b23(a16(b14(a13(b22(x1)))))) (3304)
a10(b21(c25(b17(a14(a22(x1)))))) → a10(b21(c16(b14(a13(b22(x1)))))) (3331)
a13(b22(b25(b17(a14(a22(x1)))))) → a13(b22(b16(b14(a13(b22(x1)))))) (3358)
c17(a23(a25(b17(a14(a22(x1)))))) → c17(a23(a16(b14(a13(b22(x1)))))) (3385)
c11(a21(c25(b17(a14(a22(x1)))))) → c11(a21(c16(b14(a13(b22(x1)))))) (3412)
c14(a22(b25(b17(a14(a22(x1)))))) → c14(a22(b16(b14(a13(b22(x1)))))) (3439)
c15(c23(a25(b17(a14(a22(x1)))))) → c15(c23(a16(b14(a13(b22(x1)))))) (3466)
c9(c21(c25(b17(a14(a22(x1)))))) → c9(c21(c16(b14(a13(b22(x1)))))) (3493)
c12(c22(b25(b17(a14(a22(x1)))))) → c12(c22(b16(b14(a13(b22(x1)))))) (3520)
c16(b23(a25(b17(a14(a22(x1)))))) → c16(b23(a16(b14(a13(b22(x1)))))) (3547)
c10(b21(c25(b17(a14(a22(x1)))))) → c10(b21(c16(b14(a13(b22(x1)))))) (3574)
c13(b22(b25(b17(a14(a22(x1)))))) → c13(b22(b16(b14(a13(b22(x1)))))) (3601)
b17(a23(a25(b17(a14(a22(x1)))))) → b17(a23(a16(b14(a13(b22(x1)))))) (3628)
b11(a21(c25(b17(a14(a22(x1)))))) → b11(a21(c16(b14(a13(b22(x1)))))) (3655)
b14(a22(b25(b17(a14(a22(x1)))))) → b14(a22(b16(b14(a13(b22(x1)))))) (3682)
b15(c23(a25(b17(a14(a22(x1)))))) → b15(c23(a16(b14(a13(b22(x1)))))) (3709)
b9(c21(c25(b17(a14(a22(x1)))))) → b9(c21(c16(b14(a13(b22(x1)))))) (3736)
b12(c22(b25(b17(a14(a22(x1)))))) → b12(c22(b16(b14(a13(b22(x1)))))) (3763)
b16(b23(a25(b17(a14(a22(x1)))))) → b16(b23(a16(b14(a13(b22(x1)))))) (3790)
b10(b21(c25(b17(a14(a22(x1)))))) → b10(b21(c16(b14(a13(b22(x1)))))) (3817)
b13(b22(b25(b17(a14(a22(x1)))))) → b13(b22(b16(b14(a13(b22(x1)))))) (3844)

1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.