Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96563)

The rewrite relation of the following TRS is considered.

0(1(2(3(x1)))) → 0(2(2(3(x1)))) (1)
1(1(4(4(5(x1))))) → 5(1(0(0(5(x1))))) (2)
2(3(3(2(5(x1))))) → 3(5(4(5(5(x1))))) (3)
5(1(1(5(3(x1))))) → 5(1(4(5(3(x1))))) (4)
0(2(5(1(1(4(x1)))))) → 0(3(2(2(4(5(x1)))))) (5)
1(2(1(4(0(3(x1)))))) → 4(2(5(4(5(3(x1)))))) (6)
1(5(2(0(4(3(x1)))))) → 5(0(1(1(1(x1))))) (7)
2(2(1(5(4(0(x1)))))) → 2(3(5(4(0(3(x1)))))) (8)
4(0(2(3(1(4(4(x1))))))) → 4(1(3(0(5(0(5(x1))))))) (9)
4(3(5(4(3(2(2(2(x1)))))))) → 4(1(2(3(4(1(4(x1))))))) (10)
0(2(2(2(3(4(3(3(3(x1))))))))) → 0(5(4(0(5(3(5(5(3(x1))))))))) (11)
4(5(3(4(1(1(0(5(2(x1))))))))) → 4(4(3(1(3(2(0(5(2(x1))))))))) (12)
3(3(4(1(0(4(5(1(5(2(x1)))))))))) → 3(3(4(1(5(0(3(0(2(4(x1)))))))))) (13)
2(4(5(4(0(5(5(1(2(1(4(2(x1)))))))))))) → 4(1(0(1(1(3(3(0(1(4(2(x1))))))))))) (14)
1(0(0(4(5(4(3(4(5(1(5(4(0(x1))))))))))))) → 5(3(3(1(2(1(1(0(3(1(3(x1))))))))))) (15)
1(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4(4(4(3(2(0(1(3(1(2(2(4(5(x1))))))))))))) (16)
4(1(5(4(5(3(3(3(1(2(0(2(0(x1))))))))))))) → 4(1(4(3(4(4(0(1(3(1(1(5(x1)))))))))))) (17)
2(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 5(5(5(2(0(2(5(0(0(4(3(2(1(4(3(3(1(x1))))))))))))))))) (18)
1(5(1(1(3(0(3(3(3(3(1(1(5(1(5(2(5(2(x1)))))))))))))))))) → 3(5(4(2(0(5(1(3(4(1(1(2(5(2(4(1(5(2(x1)))))))))))))))))) (19)
2(4(3(3(4(2(3(5(4(0(4(0(2(3(0(3(3(0(x1)))))))))))))))))) → 2(1(3(0(4(4(1(5(2(1(0(3(0(5(0(1(5(x1))))))))))))))))) (20)
2(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2(1(5(0(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1)))))))))))))))))) (21)
2(3(5(1(3(0(0(5(0(2(2(4(5(4(0(3(1(4(2(x1))))))))))))))))))) → 5(2(0(2(0(3(2(3(5(2(2(4(1(3(5(5(1(2(x1)))))))))))))))))) (22)
3(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 3(2(0(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))))))))) (23)
3(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3(1(3(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))))))) (24)
4(5(1(4(5(3(1(5(5(3(5(0(2(1(2(4(4(5(1(0(4(x1))))))))))))))))))))) → 4(4(0(2(1(5(2(0(4(5(2(2(3(5(5(2(2(0(3(5(4(x1))))))))))))))))))))) (25)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[5(x1)] = x1 +
5
[4(x1)] = x1 +
5
[3(x1)] = x1 +
5
[2(x1)] = x1 +
5
[1(x1)] = x1 +
6
[0(x1)] = x1 +
5
all of the following rules can be deleted.
0(1(2(3(x1)))) → 0(2(2(3(x1)))) (1)
1(1(4(4(5(x1))))) → 5(1(0(0(5(x1))))) (2)
5(1(1(5(3(x1))))) → 5(1(4(5(3(x1))))) (4)
0(2(5(1(1(4(x1)))))) → 0(3(2(2(4(5(x1)))))) (5)
1(2(1(4(0(3(x1)))))) → 4(2(5(4(5(3(x1)))))) (6)
1(5(2(0(4(3(x1)))))) → 5(0(1(1(1(x1))))) (7)
2(2(1(5(4(0(x1)))))) → 2(3(5(4(0(3(x1)))))) (8)
4(3(5(4(3(2(2(2(x1)))))))) → 4(1(2(3(4(1(4(x1))))))) (10)
4(5(3(4(1(1(0(5(2(x1))))))))) → 4(4(3(1(3(2(0(5(2(x1))))))))) (12)
3(3(4(1(0(4(5(1(5(2(x1)))))))))) → 3(3(4(1(5(0(3(0(2(4(x1)))))))))) (13)
2(4(5(4(0(5(5(1(2(1(4(2(x1)))))))))))) → 4(1(0(1(1(3(3(0(1(4(2(x1))))))))))) (14)
1(0(0(4(5(4(3(4(5(1(5(4(0(x1))))))))))))) → 5(3(3(1(2(1(1(0(3(1(3(x1))))))))))) (15)
4(1(5(4(5(3(3(3(1(2(0(2(0(x1))))))))))))) → 4(1(4(3(4(4(0(1(3(1(1(5(x1)))))))))))) (17)
1(5(1(1(3(0(3(3(3(3(1(1(5(1(5(2(5(2(x1)))))))))))))))))) → 3(5(4(2(0(5(1(3(4(1(1(2(5(2(4(1(5(2(x1)))))))))))))))))) (19)
2(4(3(3(4(2(3(5(4(0(4(0(2(3(0(3(3(0(x1)))))))))))))))))) → 2(1(3(0(4(4(1(5(2(1(0(3(0(5(0(1(5(x1))))))))))))))))) (20)
2(3(5(1(3(0(0(5(0(2(2(4(5(4(0(3(1(4(2(x1))))))))))))))))))) → 5(2(0(2(0(3(2(3(5(2(2(4(1(3(5(5(1(2(x1)))))))))))))))))) (22)
4(5(1(4(5(3(1(5(5(3(5(0(2(1(2(4(4(5(1(0(4(x1))))))))))))))))))))) → 4(4(0(2(1(5(2(0(4(5(2(2(3(5(5(2(2(0(3(5(4(x1))))))))))))))))))))) (25)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
4#(0(2(3(1(4(4(x1))))))) → 4#(1(3(0(5(0(5(x1))))))) (26)
4#(0(2(3(1(4(4(x1))))))) → 3#(0(5(0(5(x1))))) (27)
4#(0(2(3(1(4(4(x1))))))) → 1#(3(0(5(0(5(x1)))))) (28)
4#(0(2(3(1(4(4(x1))))))) → 0#(5(x1)) (29)
4#(0(2(3(1(4(4(x1))))))) → 0#(5(0(5(x1)))) (30)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(5(2(4(3(x1))))) (31)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(3(x1)) (32)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))) (33)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))) (34)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(5(0(3(4(5(2(4(3(x1))))))))) (35)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(4(5(2(4(3(x1)))))) (36)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))))) (37)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(1(3(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))))))) (38)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1))))))))))))))))) (39)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 2#(4(3(x1))) (40)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 2#(4(1(2(3(5(0(3(4(5(2(4(3(x1))))))))))))) (41)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 2#(3(5(0(3(4(5(2(4(3(x1)))))))))) (42)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 1#(3(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1))))))))))))))))))) (43)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 1#(2(3(5(0(3(4(5(2(4(3(x1))))))))))) (44)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 0#(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))) (45)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 0#(3(4(5(2(4(3(x1))))))) (46)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 4#(2(5(2(2(4(x1)))))) (47)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 3#(2(0(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))))))))) (48)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 3#(0(2(4(2(5(2(2(4(x1))))))))) (49)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(5(2(2(4(x1))))) (50)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(4(x1)) (51)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(4(2(5(2(2(4(x1))))))) (52)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(3(0(2(4(2(5(2(2(4(x1)))))))))) (53)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(2(4(x1))) (54)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(0(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1))))))))))))))))))) (55)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 1#(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))) (56)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 1#(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1))))))))))))))))) (57)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 1#(2(3(0(2(4(2(5(2(2(4(x1))))))))))) (58)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 0#(2(4(2(5(2(2(4(x1)))))))) (59)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 0#(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1))))))))))))))) (60)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 0#(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))))))) (61)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 4#(3(3(x1))) (62)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 3#(x1) (63)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 3#(3(x1)) (64)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 3#(1(0(5(0(4(3(3(x1)))))))) (65)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(3(1(0(5(0(4(3(3(x1))))))))) (66)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(2(3(1(0(5(0(4(3(3(x1)))))))))) (67)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(2(2(3(1(0(5(0(4(3(3(x1))))))))))) (68)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(1(5(0(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1)))))))))))))))))) (69)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 1#(5(2(2(2(3(1(0(5(0(4(3(3(x1))))))))))))) (70)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 1#(5(0(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1))))))))))))))))) (71)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 1#(0(5(0(4(3(3(x1))))))) (72)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(5(0(4(3(3(x1)))))) (73)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(4(3(3(x1)))) (74)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(1(5(2(2(2(3(1(0(5(0(4(3(3(x1)))))))))))))) (75)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1))))))))))))))) (76)
2#(3(3(2(5(x1))))) → 4#(5(5(x1))) (77)
2#(3(3(2(5(x1))))) → 3#(5(4(5(5(x1))))) (78)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 4#(3(3(1(x1)))) (79)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 4#(3(2(1(4(3(3(1(x1)))))))) (80)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 3#(3(1(x1))) (81)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 3#(2(1(4(3(3(1(x1))))))) (82)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 2#(5(0(0(4(3(2(1(4(3(3(1(x1)))))))))))) (83)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 2#(1(4(3(3(1(x1)))))) (84)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 2#(0(2(5(0(0(4(3(2(1(4(3(3(1(x1)))))))))))))) (85)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 1#(4(3(3(1(x1))))) (86)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 0#(4(3(2(1(4(3(3(1(x1))))))))) (87)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 0#(2(5(0(0(4(3(2(1(4(3(3(1(x1))))))))))))) (88)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 0#(0(4(3(2(1(4(3(3(1(x1)))))))))) (89)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(5(x1)) (90)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(4(4(3(2(0(1(3(1(2(2(4(5(x1))))))))))))) (91)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(4(3(2(0(1(3(1(2(2(4(5(x1)))))))))))) (92)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(3(2(0(1(3(1(2(2(4(5(x1))))))))))) (93)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 3#(2(0(1(3(1(2(2(4(5(x1)))))))))) (94)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 3#(1(2(2(4(5(x1)))))) (95)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 2#(4(5(x1))) (96)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 2#(2(4(5(x1)))) (97)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 2#(0(1(3(1(2(2(4(5(x1))))))))) (98)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 1#(3(1(2(2(4(5(x1))))))) (99)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 1#(2(2(4(5(x1))))) (100)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 0#(1(3(1(2(2(4(5(x1)))))))) (101)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 4#(0(5(3(5(5(3(x1))))))) (102)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 3#(5(5(3(x1)))) (103)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 0#(5(4(0(5(3(5(5(3(x1))))))))) (104)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 0#(5(3(5(5(3(x1)))))) (105)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[5(x1)] = x1 +
2
[4(x1)] = x1 +
2
[3(x1)] = x1 +
2
[2(x1)] = x1 +
2
[1(x1)] = x1 +
2
[0(x1)] = x1 +
2
[4#(x1)] = x1 +
0
[3#(x1)] = x1 +
2
[2#(x1)] = x1 +
3
[1#(x1)] = x1 +
1
[0#(x1)] = x1 +
0
together with the usable rules
2(3(3(2(5(x1))))) → 3(5(4(5(5(x1))))) (3)
4(0(2(3(1(4(4(x1))))))) → 4(1(3(0(5(0(5(x1))))))) (9)
0(2(2(2(3(4(3(3(3(x1))))))))) → 0(5(4(0(5(3(5(5(3(x1))))))))) (11)
1(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4(4(4(3(2(0(1(3(1(2(2(4(5(x1))))))))))))) (16)
2(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 5(5(5(2(0(2(5(0(0(4(3(2(1(4(3(3(1(x1))))))))))))))))) (18)
2(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2(1(5(0(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1)))))))))))))))))) (21)
3(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 3(2(0(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))))))))) (23)
3(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3(1(3(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))))))) (24)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
4#(0(2(3(1(4(4(x1))))))) → 3#(0(5(0(5(x1))))) (27)
4#(0(2(3(1(4(4(x1))))))) → 1#(3(0(5(0(5(x1)))))) (28)
4#(0(2(3(1(4(4(x1))))))) → 0#(5(x1)) (29)
4#(0(2(3(1(4(4(x1))))))) → 0#(5(0(5(x1)))) (30)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(5(2(4(3(x1))))) (31)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(3(x1)) (32)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))) (33)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 4#(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))) (34)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(5(0(3(4(5(2(4(3(x1))))))))) (35)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(4(5(2(4(3(x1)))))) (36)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))))) (37)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 3#(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1))))))))))))))))) (39)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 2#(4(3(x1))) (40)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 2#(4(1(2(3(5(0(3(4(5(2(4(3(x1))))))))))))) (41)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 2#(3(5(0(3(4(5(2(4(3(x1)))))))))) (42)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 1#(3(3(0(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1))))))))))))))))))) (43)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 1#(2(3(5(0(3(4(5(2(4(3(x1))))))))))) (44)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 0#(5(4(2(4(1(2(3(5(0(3(4(5(2(4(3(x1)))))))))))))))) (45)
3#(5(5(2(0(4(4(5(5(0(3(5(2(1(2(1(0(2(2(3(x1)))))))))))))))))))) → 0#(3(4(5(2(4(3(x1))))))) (46)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 4#(2(5(2(2(4(x1)))))) (47)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 3#(0(2(4(2(5(2(2(4(x1))))))))) (49)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(5(2(2(4(x1))))) (50)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(4(x1)) (51)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(4(2(5(2(2(4(x1))))))) (52)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(3(0(2(4(2(5(2(2(4(x1)))))))))) (53)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(2(4(x1))) (54)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 2#(0(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1))))))))))))))))))) (55)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 1#(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))) (56)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 1#(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1))))))))))))))))) (57)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 1#(2(3(0(2(4(2(5(2(2(4(x1))))))))))) (58)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 0#(2(4(2(5(2(2(4(x1)))))))) (59)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 0#(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1))))))))))))))) (60)
3#(2(3(4(1(2(5(5(0(1(2(3(4(0(5(1(4(4(5(4(x1)))))))))))))))))))) → 0#(1(5(0(1(5(5(1(2(3(0(2(4(2(5(2(2(4(x1)))))))))))))))))) (61)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 4#(3(3(x1))) (62)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 3#(x1) (63)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 3#(3(x1)) (64)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 3#(1(0(5(0(4(3(3(x1)))))))) (65)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(3(1(0(5(0(4(3(3(x1))))))))) (66)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(2(3(1(0(5(0(4(3(3(x1)))))))))) (67)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 2#(2(2(3(1(0(5(0(4(3(3(x1))))))))))) (68)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 1#(5(2(2(2(3(1(0(5(0(4(3(3(x1))))))))))))) (70)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 1#(5(0(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1))))))))))))))))) (71)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 1#(0(5(0(4(3(3(x1))))))) (72)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(5(0(4(3(3(x1)))))) (73)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(4(3(3(x1)))) (74)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(1(5(2(2(2(3(1(0(5(0(4(3(3(x1)))))))))))))) (75)
2#(5(5(1(2(3(5(0(3(0(0(3(3(1(0(1(3(2(x1)))))))))))))))))) → 0#(0(1(5(2(2(2(3(1(0(5(0(4(3(3(x1))))))))))))))) (76)
2#(3(3(2(5(x1))))) → 4#(5(5(x1))) (77)
2#(3(3(2(5(x1))))) → 3#(5(4(5(5(x1))))) (78)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 4#(3(3(1(x1)))) (79)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 4#(3(2(1(4(3(3(1(x1)))))))) (80)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 3#(3(1(x1))) (81)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 3#(2(1(4(3(3(1(x1))))))) (82)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 2#(5(0(0(4(3(2(1(4(3(3(1(x1)))))))))))) (83)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 2#(1(4(3(3(1(x1)))))) (84)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 2#(0(2(5(0(0(4(3(2(1(4(3(3(1(x1)))))))))))))) (85)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 1#(4(3(3(1(x1))))) (86)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 0#(4(3(2(1(4(3(3(1(x1))))))))) (87)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 0#(2(5(0(0(4(3(2(1(4(3(3(1(x1))))))))))))) (88)
2#(2(3(3(0(2(0(2(5(0(5(5(5(1(0(3(1(x1))))))))))))))))) → 0#(0(4(3(2(1(4(3(3(1(x1)))))))))) (89)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(5(x1)) (90)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(4(4(3(2(0(1(3(1(2(2(4(5(x1))))))))))))) (91)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(4(3(2(0(1(3(1(2(2(4(5(x1)))))))))))) (92)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 4#(3(2(0(1(3(1(2(2(4(5(x1))))))))))) (93)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 3#(2(0(1(3(1(2(2(4(5(x1)))))))))) (94)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 3#(1(2(2(4(5(x1)))))) (95)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 2#(4(5(x1))) (96)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 2#(2(4(5(x1)))) (97)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 2#(0(1(3(1(2(2(4(5(x1))))))))) (98)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 1#(3(1(2(2(4(5(x1))))))) (99)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 1#(2(2(4(5(x1))))) (100)
1#(2(2(1(2(3(2(4(4(0(0(3(2(x1))))))))))))) → 0#(1(3(1(2(2(4(5(x1)))))))) (101)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 4#(0(5(3(5(5(3(x1))))))) (102)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 3#(5(5(3(x1)))) (103)
0#(2(2(2(3(4(3(3(3(x1))))))))) → 0#(5(3(5(5(3(x1)))))) (105)
and no rules could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.