Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/135659)

The rewrite relation of the following TRS is considered.

0(0(0(0(0(0(0(0(1(0(0(0(0(0(1(1(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(1(0(1(0(0(1(0(0(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (1)
0(0(0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(x1)))))))))))))))))))) → 1(1(0(0(0(0(0(0(0(0(0(0(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) (2)
0(0(0(0(0(0(0(1(1(1(1(0(0(0(0(1(0(1(0(0(x1)))))))))))))))))))) → 0(1(0(0(0(0(0(0(1(0(0(1(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) (3)
0(0(0(0(0(0(1(0(0(0(0(1(1(1(1(1(0(0(0(1(x1)))))))))))))))))))) → 0(0(1(0(0(0(0(0(1(1(0(0(0(0(0(0(1(0(0(1(x1)))))))))))))))))))) (4)
0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(0(1(1(x1)))))))))))))))))))) → 0(1(1(0(1(0(1(0(0(1(1(0(0(0(0(0(0(1(1(1(x1)))))))))))))))))))) (5)
0(0(0(0(0(0(1(0(0(1(0(1(1(0(1(1(1(0(0(1(x1)))))))))))))))))))) → 0(1(0(0(1(0(1(0(1(0(0(1(0(1(0(0(0(1(1(0(x1)))))))))))))))))))) (6)
0(0(0(0(0(0(1(1(0(1(1(0(0(0(0(0(1(1(0(1(x1)))))))))))))))))))) → 0(0(1(0(1(1(0(0(0(1(0(1(0(1(0(0(0(1(0(0(x1)))))))))))))))))))) (7)
0(0(0(0(0(1(1(1(0(0(0(1(0(0(1(1(1(0(1(0(x1)))))))))))))))))))) → 1(1(1(0(0(1(0(0(0(1(0(0(0(0(1(0(0(0(0(1(x1)))))))))))))))))))) (8)
0(0(0(0(1(0(0(0(1(1(0(0(1(0(1(1(0(1(1(1(x1)))))))))))))))))))) → 0(0(1(0(1(0(0(0(1(0(0(1(1(1(1(0(1(0(0(0(x1)))))))))))))))))))) (9)
0(0(0(0(1(1(1(0(0(0(0(1(0(0(0(1(0(1(1(1(x1)))))))))))))))))))) → 0(1(0(0(1(1(0(1(0(1(1(0(0(0(0(0(0(0(1(1(x1)))))))))))))))))))) (10)
0(0(0(1(0(0(0(0(0(0(1(0(1(0(1(1(1(1(0(0(x1)))))))))))))))))))) → 1(1(0(0(0(1(0(1(0(0(0(0(0(1(0(0(1(0(0(0(x1)))))))))))))))))))) (11)
0(0(0(1(0(0(0(1(0(1(1(1(0(0(1(0(1(0(1(1(x1)))))))))))))))))))) → 0(0(0(0(0(1(1(1(0(0(0(0(1(1(1(0(0(1(0(0(x1)))))))))))))))))))) (12)
0(0(0(1(0(1(1(1(0(1(0(0(0(1(1(0(0(1(0(1(x1)))))))))))))))))))) → 1(0(0(0(1(0(1(1(0(0(0(0(0(0(0(1(1(1(0(0(x1)))))))))))))))))))) (13)
0(0(0(1(1(0(0(0(1(1(0(0(1(1(0(0(0(1(0(1(x1)))))))))))))))))))) → 0(0(0(1(0(0(1(1(0(0(0(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))) (14)
0(0(0(1(1(0(1(0(1(1(0(0(1(0(1(0(1(0(0(1(x1)))))))))))))))))))) → 1(0(0(0(1(1(0(1(0(1(0(0(0(0(0(1(0(1(0(0(x1)))))))))))))))))))) (15)
0(0(0(1(1(1(1(1(0(0(0(1(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) → 0(1(1(0(0(0(1(0(0(0(1(0(0(1(0(1(1(0(0(0(x1)))))))))))))))))))) (16)
0(0(1(0(0(0(0(1(0(0(0(1(0(0(0(1(0(1(1(1(x1)))))))))))))))))))) → 0(1(0(1(0(0(0(0(0(0(0(0(1(1(0(0(0(0(1(1(x1)))))))))))))))))))) (17)
0(0(1(0(0(0(0(1(0(0(0(1(1(1(0(1(1(0(0(0(x1)))))))))))))))))))) → 0(1(0(0(0(1(0(1(1(0(0(1(0(0(0(1(0(0(1(0(x1)))))))))))))))))))) (18)
0(0(1(0(0(0(1(0(0(1(0(1(1(1(0(0(1(0(0(1(x1)))))))))))))))))))) → 0(0(0(1(0(0(1(0(0(0(0(0(1(0(0(0(0(1(0(0(x1)))))))))))))))))))) (19)
0(0(1(0(0(1(0(1(1(1(0(0(0(0(1(1(0(0(0(1(x1)))))))))))))))))))) → 1(0(0(1(0(0(1(1(0(1(0(0(1(0(0(1(0(0(0(1(x1)))))))))))))))))))) (20)
0(0(1(0(0(1(1(0(0(0(0(1(0(1(1(0(0(1(0(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(0(0(0(0(0(1(0(1(0(0(0(0(0(1(x1)))))))))))))))))))) (21)
0(0(1(0(0(1(1(0(0(1(0(0(0(1(1(0(1(0(0(1(x1)))))))))))))))))))) → 0(1(0(1(0(1(0(0(0(0(0(1(0(0(1(0(1(0(1(0(x1)))))))))))))))))))) (22)
0(0(1(0(1(0(0(1(1(0(1(0(1(0(0(0(1(1(1(0(x1)))))))))))))))))))) → 0(1(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(0(1(0(x1)))))))))))))))))))) (23)
0(0(1(0(1(0(1(0(0(0(1(0(1(1(1(0(1(1(0(0(x1)))))))))))))))))))) → 1(0(0(0(1(1(1(0(0(1(0(0(0(0(0(1(1(0(1(0(x1)))))))))))))))))))) (24)
0(0(1(0(1(0(1(0(1(1(0(0(1(0(1(0(0(0(1(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(0(0(0(1(1(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) (25)
0(0(1(0(1(1(0(0(0(0(0(1(1(0(0(0(1(0(1(1(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(0(1(0(0(0(0(0(1(0(0(0(0(1(x1)))))))))))))))))))) (26)
0(0(1(0(1(1(0(0(1(1(1(1(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 0(1(0(0(1(0(1(1(1(0(0(0(1(0(1(1(0(0(0(0(x1)))))))))))))))))))) (27)
0(0(1(0(1(1(1(0(0(0(0(0(0(1(1(0(0(1(0(1(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(1(0(0(1(1(0(1(0(1(0(0(0(1(x1)))))))))))))))))))) (28)
0(0(1(0(1(1(1(0(0(1(1(1(0(0(1(0(0(1(0(1(x1)))))))))))))))))))) → 1(0(1(0(1(1(0(0(0(1(1(0(1(0(1(1(0(0(0(1(x1)))))))))))))))))))) (29)
0(0(1(0(1(1(1(1(0(1(0(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 1(0(0(1(0(0(0(0(0(0(1(0(1(0(1(1(0(0(0(1(x1)))))))))))))))))))) (30)
0(0(1(1(0(0(0(1(0(0(1(1(1(1(0(0(0(0(1(0(x1)))))))))))))))))))) → 1(1(0(0(0(0(0(0(1(0(1(0(1(0(1(0(1(1(0(0(x1)))))))))))))))))))) (31)
0(0(1(1(0(0(1(0(0(1(0(0(1(0(1(0(0(0(1(1(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(1(0(0(0(0(1(1(0(0(0(0(1(0(x1)))))))))))))))))))) (32)
0(0(1(1(0(0(1(0(0(1(0(1(0(0(1(1(0(1(0(0(x1)))))))))))))))))))) → 0(1(1(0(0(1(0(1(0(1(1(0(1(0(1(0(0(0(0(0(x1)))))))))))))))))))) (33)
0(0(1(1(0(1(1(1(0(0(0(0(1(1(0(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(1(1(0(0(0(0(0(1(1(1(0(1(1(0(1(0(0(0(x1)))))))))))))))))))) (34)
0(0(1(1(1(0(1(0(1(0(1(0(0(0(1(0(0(0(1(0(x1)))))))))))))))))))) → 0(0(1(1(0(1(0(0(1(0(1(0(0(1(1(0(0(1(0(0(x1)))))))))))))))))))) (35)
0(0(1(1(1(1(0(0(0(0(0(0(0(1(0(0(1(1(0(1(x1)))))))))))))))))))) → 0(1(0(0(0(1(0(0(1(1(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (36)
0(1(0(0(0(0(0(0(0(1(0(1(0(1(0(1(1(1(0(1(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(1(0(1(0(0(1(0(0(1(0(0(1(0(x1)))))))))))))))))))) (37)
0(1(0(0(0(0(0(0(1(0(1(1(1(0(0(1(0(0(1(1(x1)))))))))))))))))))) → 0(1(0(1(0(0(0(1(0(0(0(0(1(1(0(0(0(0(1(0(x1)))))))))))))))))))) (38)
0(1(0(0(0(0(1(0(0(1(0(0(1(0(1(1(0(1(1(0(x1)))))))))))))))))))) → 1(0(0(0(1(1(0(0(0(1(0(1(0(0(0(0(0(0(0(0(x1)))))))))))))))))))) (39)
0(1(0(0(0(0(1(1(1(0(1(0(1(0(1(0(1(0(0(1(x1)))))))))))))))))))) → 1(0(1(0(0(1(0(0(1(0(0(0(0(1(0(1(0(1(0(1(x1)))))))))))))))))))) (40)
0(1(0(0(0(1(1(0(0(1(1(0(0(0(1(1(0(1(0(1(x1)))))))))))))))))))) → 1(0(0(1(0(0(0(1(1(0(1(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))) (41)
0(1(0(0(1(0(0(0(0(0(0(1(1(1(0(1(0(0(1(1(x1)))))))))))))))))))) → 0(0(0(0(1(0(0(0(0(0(1(0(0(1(1(0(1(0(1(0(x1)))))))))))))))))))) (42)
0(1(0(0(1(0(0(0(0(0(1(1(0(0(0(1(0(1(1(1(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(0(0(0(0(0(0(1(0(1(0(1(1(1(x1)))))))))))))))))))) (43)
0(1(0(0(1(0(0(0(1(0(1(0(0(0(1(1(1(0(1(0(x1)))))))))))))))))))) → 1(1(0(0(0(0(0(0(1(1(0(0(0(0(0(0(0(1(1(0(x1)))))))))))))))))))) (44)
0(1(0(0(1(0(0(1(0(0(0(0(0(0(1(1(1(0(0(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(1(0(1(0(0(0(0(1(0(0(0(0(1(1(x1)))))))))))))))))))) (45)
0(1(0(0(1(0(0(1(0(1(0(1(1(0(1(0(0(0(1(1(x1)))))))))))))))))))) → 0(0(0(0(0(1(1(1(0(0(0(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))) (46)
0(1(0(0(1(0(1(0(0(0(1(0(0(1(1(1(0(0(1(0(x1)))))))))))))))))))) → 1(0(1(1(0(0(0(0(0(0(1(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))) (47)
0(1(0(0(1(0(1(0(0(1(0(0(0(0(1(1(1(0(1(1(x1)))))))))))))))))))) → 1(1(0(0(1(0(0(1(0(0(0(0(1(0(1(0(0(1(0(0(x1)))))))))))))))))))) (48)
0(1(0(0(1(0(1(0(0(1(0(1(0(1(1(0(0(1(0(1(x1)))))))))))))))))))) → 0(0(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(0(1(x1)))))))))))))))))))) (49)
0(1(0(0(1(0(1(0(1(1(0(1(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 0(0(1(0(0(0(0(1(0(0(1(0(0(1(0(0(1(0(0(0(x1)))))))))))))))))))) (50)
0(1(0(0(1(0(1(1(0(0(0(0(0(0(1(0(1(1(0(0(x1)))))))))))))))))))) → 0(0(1(0(1(0(0(1(0(0(0(1(0(1(1(0(0(0(0(0(x1)))))))))))))))))))) (51)
0(1(0(0(1(1(0(1(0(0(0(1(1(0(1(0(1(0(0(1(x1)))))))))))))))))))) → 0(1(0(1(0(0(1(0(0(0(1(1(1(0(0(1(0(1(0(0(x1)))))))))))))))))))) (52)
0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(0(1(0(0(1(x1)))))))))))))))))))) → 0(0(0(1(0(1(0(0(0(0(0(1(0(0(0(0(1(1(0(1(x1)))))))))))))))))))) (53)
0(1(0(1(0(0(1(0(1(1(0(0(1(0(0(0(1(0(1(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(0(0(0(0(0(0(1(0(1(0(1(1(1(1(x1)))))))))))))))))))) (54)
0(1(0(1(0(1(1(1(0(0(0(1(1(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 1(1(1(0(1(0(1(0(0(0(0(0(0(0(1(0(0(0(0(0(x1)))))))))))))))))))) (55)
0(1(0(1(1(0(0(0(0(0(1(0(1(1(1(0(0(1(0(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(1(0(1(0(0(1(0(1(1(1(0(1(0(0(x1)))))))))))))))))))) (56)
0(1(0(1(1(0(0(1(0(1(1(0(0(1(0(0(0(1(0(1(x1)))))))))))))))))))) → 0(0(0(0(0(1(1(0(0(1(0(1(0(0(1(0(1(1(0(0(x1)))))))))))))))))))) (57)
0(1(0(1(1(1(0(1(0(0(0(0(0(1(0(0(0(0(1(1(x1)))))))))))))))))))) → 0(0(1(0(0(0(0(0(1(0(0(1(0(0(0(1(1(1(0(1(x1)))))))))))))))))))) (58)
0(1(1(0(0(0(0(0(0(1(1(0(0(1(1(1(0(0(0(1(x1)))))))))))))))))))) → 1(0(0(0(0(1(0(0(0(1(1(0(0(0(0(0(1(0(1(0(x1)))))))))))))))))))) (59)
0(1(1(0(0(0(0(1(0(0(0(0(0(0(1(1(1(0(1(0(x1)))))))))))))))))))) → 0(1(1(0(0(0(0(0(1(0(0(1(0(0(0(0(1(0(1(0(x1)))))))))))))))))))) (60)
0(1(1(0(0(0(0(1(0(0(0(0(1(0(0(1(0(0(1(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(0(0(0(0(0(0(1(0(0(0(0(0(1(x1)))))))))))))))))))) (61)
0(1(1(0(0(0(0(1(1(1(0(0(0(0(0(1(1(0(0(1(x1)))))))))))))))))))) → 1(0(0(0(0(1(1(1(0(1(0(1(0(0(0(1(0(0(0(1(x1)))))))))))))))))))) (62)
0(1(1(0(0(0(1(0(0(1(0(0(0(0(1(1(1(0(1(1(x1)))))))))))))))))))) → 1(0(0(0(1(0(1(0(1(0(1(0(0(0(0(1(1(0(1(1(x1)))))))))))))))))))) (63)
0(1(1(0(0(0(1(1(0(1(0(0(1(0(0(0(1(0(0(1(x1)))))))))))))))))))) → 0(1(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(0(0(0(x1)))))))))))))))))))) (64)
0(1(1(0(0(0(1(1(1(0(0(1(1(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 0(1(0(1(1(0(1(0(0(0(0(1(1(0(1(0(0(0(0(1(x1)))))))))))))))))))) (65)
0(1(1(0(1(0(0(1(0(1(1(0(0(0(0(0(1(0(1(1(x1)))))))))))))))))))) → 1(0(1(0(1(0(1(0(0(1(0(0(0(0(1(0(0(1(0(0(x1)))))))))))))))))))) (66)
0(1(1(1(0(0(1(0(0(0(1(0(1(0(0(0(0(1(0(1(x1)))))))))))))))))))) → 0(1(1(0(1(0(1(0(0(0(0(1(0(1(1(0(0(0(0(1(x1)))))))))))))))))))) (67)
0(1(1(1(0(1(0(0(1(0(0(0(1(0(0(0(1(0(1(1(x1)))))))))))))))))))) → 1(0(1(1(0(0(1(0(0(0(1(0(0(0(0(1(0(1(0(1(x1)))))))))))))))))))) (68)
0(1(1(1(0(1(1(0(0(0(0(0(0(1(1(0(1(0(1(1(x1)))))))))))))))))))) → 1(1(0(0(0(1(0(0(0(1(0(1(1(0(1(0(0(1(1(0(x1)))))))))))))))))))) (69)
1(0(0(0(0(0(0(1(1(0(1(0(0(1(1(0(1(0(0(0(x1)))))))))))))))))))) → 0(1(0(1(0(0(1(0(1(0(0(1(0(0(0(0(0(1(0(0(x1)))))))))))))))))))) (70)
1(0(0(0(0(0(1(0(1(0(1(0(0(1(0(1(0(1(1(1(x1)))))))))))))))))))) → 0(0(0(0(0(0(1(1(0(0(1(0(1(1(1(0(0(0(0(0(x1)))))))))))))))))))) (71)
1(0(0(0(0(0(1(1(1(0(1(0(0(0(0(0(0(1(1(1(x1)))))))))))))))))))) → 0(0(0(0(0(1(0(1(1(1(0(0(1(0(1(0(0(0(1(1(x1)))))))))))))))))))) (72)
1(0(0(0(0(1(0(0(0(1(0(0(1(1(0(1(0(1(0(1(x1)))))))))))))))))))) → 0(0(0(0(0(0(1(0(0(0(0(0(1(1(0(1(0(1(0(0(x1)))))))))))))))))))) (73)
1(0(0(0(0(1(1(0(0(0(1(1(1(0(0(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(0(0(0(0(1(0(0(0(0(1(1(0(1(0(x1)))))))))))))))))))) (74)
1(0(0(0(0(1(1(0(1(0(1(0(1(0(0(1(0(0(1(1(x1)))))))))))))))))))) → 0(1(0(1(0(0(0(0(1(1(0(0(1(0(0(0(0(1(1(0(x1)))))))))))))))))))) (75)
1(0(0(0(1(0(0(0(1(0(1(1(1(0(0(1(0(0(0(1(x1)))))))))))))))))))) → 1(0(1(1(0(0(0(0(0(1(0(0(0(1(0(0(0(1(1(0(x1)))))))))))))))))))) (76)
1(0(0(0(1(0(0(1(0(0(1(0(1(0(1(0(0(0(1(1(x1)))))))))))))))))))) → 1(0(0(1(0(0(0(1(0(0(0(0(0(1(0(0(0(1(1(1(x1)))))))))))))))))))) (77)
1(0(0(0(1(1(0(0(0(1(0(1(0(1(1(0(0(0(0(0(x1)))))))))))))))))))) → 0(1(0(1(0(1(0(0(0(0(0(0(0(1(0(1(0(0(0(1(x1)))))))))))))))))))) (78)
1(0(0(0(1(1(0(1(1(0(1(0(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(0(0(0(0(0(0(1(1(1(0(1(1(1(0(1(0(x1)))))))))))))))))))) (79)
1(0(0(0(1(1(1(0(0(1(0(0(1(0(0(1(0(0(0(0(x1)))))))))))))))))))) → 1(0(0(1(0(0(1(0(1(0(0(0(1(0(1(0(0(0(0(0(x1)))))))))))))))))))) (80)
1(0(1(0(0(0(1(1(0(0(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(1(1(0(0(1(1(0(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (81)
1(0(1(0(0(1(1(0(1(1(1(1(1(0(1(0(0(1(1(1(x1)))))))))))))))))))) → 1(0(1(0(0(1(1(1(0(1(0(1(1(0(0(1(1(0(0(1(x1)))))))))))))))))))) (82)
1(0(1(0(0(1(1(1(0(0(0(0(0(0(1(0(0(0(1(1(x1)))))))))))))))))))) → 0(0(1(1(0(0(0(0(1(0(1(0(0(0(0(1(1(0(1(0(x1)))))))))))))))))))) (83)
1(0(1(1(0(0(0(0(0(0(1(1(1(0(0(0(1(1(0(0(x1)))))))))))))))))))) → 1(1(0(1(0(0(1(0(1(1(0(1(0(0(1(0(1(0(0(0(x1)))))))))))))))))))) (84)
1(0(1(1(0(0(0(1(1(0(0(1(0(0(0(1(0(0(0(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(0(0(0(1(1(1(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) (85)
1(0(1(1(0(0(1(1(1(0(0(1(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 1(0(1(0(1(1(0(0(1(0(0(0(0(1(1(0(0(0(1(0(x1)))))))))))))))))))) (86)
1(0(1(1(1(0(0(0(0(1(0(0(0(1(0(0(1(0(0(1(x1)))))))))))))))))))) → 1(1(0(0(0(0(0(1(0(0(0(0(1(0(0(0(1(1(0(0(x1)))))))))))))))))))) (87)
1(0(1(1(1(0(0(0(1(0(0(0(1(0(0(1(0(0(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(0(0(1(0(1(0(0(0(0(1(1(1(0(x1)))))))))))))))))))) (88)
1(1(0(0(0(0(0(1(0(0(0(0(0(0(0(1(1(1(0(1(x1)))))))))))))))))))) → 1(0(1(0(0(1(0(0(0(0(1(1(0(0(0(0(0(0(1(1(x1)))))))))))))))))))) (89)
1(1(0(0(1(0(1(0(0(0(0(0(1(0(0(1(0(0(1(1(x1)))))))))))))))))))) → 0(0(1(0(0(1(1(0(0(1(0(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))) (90)
1(1(0(0(1(0(1(0(0(0(1(0(0(1(1(0(1(0(0(1(x1)))))))))))))))))))) → 1(1(1(1(0(0(0(1(0(0(0(1(1(0(0(0(0(0(0(0(x1)))))))))))))))))))) (91)
1(1(0(0(1(0(1(1(0(0(0(0(0(1(0(0(1(0(0(1(x1)))))))))))))))))))) → 0(0(1(0(0(0(1(0(0(0(0(0(0(1(1(1(0(0(0(1(x1)))))))))))))))))))) (92)
1(1(0(0(1(1(0(0(1(0(0(1(0(1(0(0(0(0(1(0(x1)))))))))))))))))))) → 0(1(0(1(0(0(0(1(1(0(1(1(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) (93)
1(1(0(0(1(1(0(0(1(1(0(0(1(0(0(0(0(0(0(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(0(0(0(0(0(1(0(1(0(1(1(0(0(x1)))))))))))))))))))) (94)
1(1(1(0(0(0(0(0(0(0(0(0(0(0(1(1(1(1(1(0(x1)))))))))))))))))))) → 1(1(0(0(1(0(0(1(1(0(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))) (95)
1(1(1(0(0(0(0(0(1(0(0(1(1(0(0(0(1(0(0(0(x1)))))))))))))))))))) → 0(1(1(0(0(0(1(0(0(1(0(0(1(0(0(0(0(0(1(0(x1)))))))))))))))))))) (96)
1(1(1(0(0(0(0(1(0(0(1(1(1(0(0(1(0(0(0(0(x1)))))))))))))))))))) → 1(1(1(1(0(0(0(0(1(0(1(0(0(1(1(0(0(0(0(0(x1)))))))))))))))))))) (97)
1(1(1(0(0(1(1(0(1(0(0(0(0(0(1(0(0(1(0(1(x1)))))))))))))))))))) → 1(0(1(0(1(0(0(1(1(1(0(0(0(0(0(1(0(1(0(1(x1)))))))))))))))))))) (98)
1(1(1(1(1(0(0(0(0(0(1(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 0(1(0(1(1(1(1(0(1(0(0(1(0(0(0(0(0(0(0(0(x1)))))))))))))))))))) (99)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{0(☐), 1(☐)}

We obtain the transformed TRS

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

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[00(x1)] = 1 · x1
[01(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[11(x1)] = 1 · x1 + 2
all of the following rules can be deleted.

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

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[00(x1)] = 1 · x1
[01(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[11(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
10(00(00(01(10(00(01(10(00(01(10(01(10(01(10(00(00(01(11(10(x1)))))))))))))))))))) → 10(00(01(10(00(00(01(10(00(00(00(00(01(10(00(00(01(11(11(10(x1)))))))))))))))))))) (272)
10(00(00(01(10(00(01(10(00(01(10(01(10(01(10(00(00(01(11(11(x1)))))))))))))))))))) → 10(00(01(10(00(00(01(10(00(00(00(00(01(10(00(00(01(11(11(11(x1)))))))))))))))))))) (273)
11(10(00(01(10(01(10(00(00(01(10(00(01(11(10(01(10(00(01(10(x1)))))))))))))))))))) → 11(11(11(10(00(00(01(10(00(00(01(11(10(00(00(00(00(00(00(00(x1)))))))))))))))))))) (288)
10(00(01(10(01(10(01(10(00(00(01(10(01(11(11(10(01(11(10(00(00(x1))))))))))))))))))))) → 11(10(00(00(01(11(11(10(00(01(10(00(00(00(00(01(11(10(01(10(00(x1))))))))))))))))))))) (328)
10(00(01(10(01(10(01(10(00(00(01(10(01(11(11(10(01(11(10(00(01(x1))))))))))))))))))))) → 11(10(00(00(01(11(11(10(00(01(10(00(00(00(00(01(11(10(01(10(01(x1))))))))))))))))))))) (329)
10(01(10(00(01(10(00(00(01(10(01(10(00(00(01(11(11(10(01(10(00(x1))))))))))))))))))))) → 11(11(10(00(00(00(00(00(01(11(10(00(00(00(00(00(00(01(11(10(00(x1))))))))))))))))))))) (368)
10(01(10(00(01(10(00(00(01(10(01(10(00(00(01(11(11(10(01(10(01(x1))))))))))))))))))))) → 11(11(10(00(00(00(00(00(01(11(10(00(00(00(00(00(00(01(11(10(01(x1))))))))))))))))))))) (369)
10(01(10(00(01(10(01(10(00(00(01(10(00(01(11(11(10(00(01(10(00(x1))))))))))))))))))))) → 11(10(01(11(10(00(00(00(00(00(01(11(10(00(01(10(00(00(01(10(00(x1))))))))))))))))))))) (376)
10(01(10(00(01(10(01(10(00(00(01(10(00(01(11(11(10(00(01(10(01(x1))))))))))))))))))))) → 11(10(01(11(10(00(00(00(00(00(01(11(10(00(01(10(00(00(01(10(01(x1))))))))))))))))))))) (377)
10(01(10(01(10(00(01(10(01(11(10(00(01(10(00(00(01(10(01(11(10(x1))))))))))))))))))))) → 11(10(00(00(00(00(00(00(00(00(00(00(01(10(01(10(01(11(11(11(10(x1))))))))))))))))))))) (384)
10(01(10(01(10(00(01(10(01(11(10(00(01(10(00(00(01(10(01(11(11(x1))))))))))))))))))))) → 11(10(00(00(00(00(00(00(00(00(00(00(01(10(01(10(01(11(11(11(11(x1))))))))))))))))))))) (385)
01(10(00(00(01(11(10(01(11(10(01(10(01(10(00(00(01(10(01(10(00(x1))))))))))))))))))))) → 00(00(00(00(00(00(00(00(00(00(01(11(11(10(01(11(11(10(01(10(00(x1))))))))))))))))))))) (450)
01(10(00(00(01(11(10(01(11(10(01(10(01(10(00(00(01(10(01(10(01(x1))))))))))))))))))))) → 00(00(00(00(00(00(00(00(00(00(01(11(11(10(01(11(11(10(01(10(01(x1))))))))))))))))))))) (451)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals
[00#(x1)] = 1
[00(x1)] = 1
[01(x1)] = 0
[10(x1)] = 0
[11(x1)] = 0
[01#(x1)] = 1
[11#(x1)] = 1
[10#(x1)] = 1 · x1
together with the usable rules
01(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(11(x1)))))))))))))))))))) → 01(11(10(01(10(01(10(00(00(00(01(10(01(11(10(00(00(00(01(11(x1)))))))))))))))))))) (269)
01(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(10(x1)))))))))))))))))))) → 01(11(10(01(10(01(10(00(00(00(01(10(01(11(10(00(00(00(01(10(x1)))))))))))))))))))) (268)
00(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(10(x1)))))))))))))))))))) → 01(11(10(01(10(01(10(00(01(11(10(00(00(00(00(00(01(11(11(10(x1)))))))))))))))))))) (200)
00(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(11(x1)))))))))))))))))))) → 01(11(10(01(10(01(10(00(01(11(10(00(00(00(00(00(01(11(11(11(x1)))))))))))))))))))) (201)
00(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(00(x1)))))))))))))))))))) → 01(10(00(00(00(01(11(10(01(11(10(01(10(00(01(11(10(01(10(00(x1)))))))))))))))))))) (224)
00(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(01(x1)))))))))))))))))))) → 01(10(00(00(00(01(11(10(01(11(10(01(10(00(01(11(10(01(10(01(x1)))))))))))))))))))) (225)
00(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 01(11(10(00(01(10(01(10(01(11(10(01(10(01(10(00(00(00(00(00(x1)))))))))))))))))))) (230)
00(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 01(11(10(00(01(10(01(10(01(11(10(01(10(01(10(00(00(00(00(01(x1)))))))))))))))))))) (231)
00(01(11(10(01(11(11(10(00(00(00(01(11(10(00(00(01(10(00(01(x1)))))))))))))))))))) → 00(01(11(10(00(00(00(00(01(11(11(10(01(11(10(01(10(00(00(01(x1)))))))))))))))))))) (233)
00(01(11(10(01(11(11(10(00(00(00(01(11(10(00(00(01(10(00(00(x1)))))))))))))))))))) → 00(01(11(10(00(00(00(00(01(11(11(10(01(11(10(01(10(00(00(00(x1)))))))))))))))))))) (232)
00(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(00(x1)))))))))))))))))))) → 00(01(11(10(01(10(00(01(10(01(10(00(01(11(10(00(01(10(00(00(x1)))))))))))))))))))) (234)
00(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(01(x1)))))))))))))))))))) → 00(01(11(10(01(10(00(01(10(01(10(00(01(11(10(00(01(10(00(01(x1)))))))))))))))))))) (235)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
00#(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(10(x1)))))))))))))))))))) → 10#(01(10(01(10(00(01(11(10(00(00(00(00(00(01(11(11(10(x1)))))))))))))))))) (488)
00#(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(10(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(00(00(00(00(00(01(11(11(10(x1)))))))))))))))) (490)
00#(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(11(x1)))))))))))))))))))) → 10#(01(10(01(10(00(01(11(10(00(00(00(00(00(01(11(11(11(x1)))))))))))))))))) (506)
00#(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(11(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(00(00(00(00(00(01(11(11(11(x1)))))))))))))))) (508)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(00(x1)))))))))))))))))))) → 10#(01(11(10(01(10(00(01(11(10(01(10(00(x1))))))))))))) (529)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(00(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(01(10(00(x1)))))))))) (532)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(00(x1)))))))))))))))))))) → 10#(01(10(00(x1)))) (538)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(01(x1)))))))))))))))))))) → 10#(01(11(10(01(10(00(01(11(10(01(10(01(x1))))))))))))) (547)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(01(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(01(10(01(x1)))))))))) (550)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(01(x1)))))))))))))))))))) → 10#(01(10(01(x1)))) (556)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 10#(01(10(01(11(10(01(10(01(10(00(00(00(00(00(x1))))))))))))))) (563)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 10#(01(11(10(01(10(01(10(00(00(00(00(00(x1))))))))))))) (565)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 10#(01(10(01(10(00(00(00(00(00(x1)))))))))) (568)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 10#(01(10(00(00(00(00(00(x1)))))))) (570)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 10#(01(10(01(11(10(01(10(01(10(00(00(00(00(01(x1))))))))))))))) (581)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 10#(01(11(10(01(10(01(10(00(00(00(00(01(x1))))))))))))) (583)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 10#(01(10(01(10(00(00(00(00(01(x1)))))))))) (586)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 10#(01(10(00(00(00(00(01(x1)))))))) (588)
00#(01(11(10(01(11(11(10(00(00(00(01(11(10(00(00(01(10(00(00(x1)))))))))))))))))))) → 10#(01(11(10(01(10(00(00(00(x1))))))))) (605)
00#(01(11(10(01(11(11(10(00(00(00(01(11(10(00(00(01(10(00(00(x1)))))))))))))))))))) → 10#(01(10(00(00(00(x1)))))) (608)
00#(01(11(10(01(11(11(10(00(00(00(01(11(10(00(00(01(10(00(01(x1)))))))))))))))))))) → 10#(01(11(10(01(10(00(00(01(x1))))))))) (623)
00#(01(11(10(01(11(11(10(00(00(00(01(11(10(00(00(01(10(00(01(x1)))))))))))))))))))) → 10#(01(10(00(00(01(x1)))))) (626)
00#(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(00(x1)))))))))))))))))))) → 10#(01(10(00(01(10(01(10(00(01(11(10(00(01(10(00(00(x1))))))))))))))))) (633)
00#(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(00(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(00(01(10(00(00(x1)))))))))))) (638)
00#(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(01(x1)))))))))))))))))))) → 10#(01(10(00(01(10(01(10(00(01(11(10(00(01(10(00(01(x1))))))))))))))))) (652)
00#(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(01(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(00(01(10(00(01(x1)))))))))))) (657)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(10(x1)))))))))))))))))))) → 10#(01(10(01(10(00(00(00(01(10(01(11(10(00(00(00(01(10(x1)))))))))))))))))) (670)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(10(x1)))))))))))))))))))) → 10#(01(10(00(00(00(01(10(01(11(10(00(00(00(01(10(x1)))))))))))))))) (672)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(10(x1)))))))))))))))))))) → 10#(01(11(10(00(00(00(01(10(x1))))))))) (679)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(11(x1)))))))))))))))))))) → 10#(01(10(01(10(00(00(00(01(10(01(11(10(00(00(00(01(11(x1)))))))))))))))))) (688)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(11(x1)))))))))))))))))))) → 10#(01(10(00(00(00(01(10(01(11(10(00(00(00(01(11(x1)))))))))))))))) (690)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(11(x1)))))))))))))))))))) → 10#(01(11(10(00(00(00(01(11(x1))))))))) (697)
11#(11(10(00(00(00(01(10(00(01(11(11(10(00(01(10(00(00(00(00(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(00(00(00(00(00(x1)))))))))))) (712)
11#(11(10(00(00(00(01(10(00(01(11(11(10(00(01(10(00(00(00(01(x1)))))))))))))))))))) → 10#(01(10(00(01(11(10(00(00(00(00(01(x1)))))))))))) (728)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(10(x1))))))))))))))))))))) → 10#(01(10(01(11(10(00(00(01(11(10(01(10(01(11(10(00(00(01(10(x1)))))))))))))))))))) (737)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(10(x1))))))))))))))))))))) → 10#(01(11(10(00(00(01(11(10(01(10(01(11(10(00(00(01(10(x1)))))))))))))))))) (739)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(10(x1))))))))))))))))))))) → 10#(01(10(01(11(10(00(00(01(10(x1)))))))))) (747)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(10(x1))))))))))))))))))))) → 10#(01(11(10(00(00(01(10(x1)))))))) (749)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(11(x1))))))))))))))))))))) → 10#(01(10(01(11(10(00(00(01(11(10(01(10(01(11(10(00(00(01(11(x1)))))))))))))))))))) (756)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(11(x1))))))))))))))))))))) → 10#(01(11(10(00(00(01(11(10(01(10(01(11(10(00(00(01(11(x1)))))))))))))))))) (758)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(11(x1))))))))))))))))))))) → 10#(01(10(01(11(10(00(00(01(11(x1)))))))))) (766)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(11(x1))))))))))))))))))))) → 10#(01(11(10(00(00(01(11(x1)))))))) (768)
could be deleted.

1.1.1.1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[00#(x1)] = 1
[00(x1)] = 1
[01(x1)] = 0
[10(x1)] = 1 · x1
[11(x1)] = 1
[01#(x1)] = 1 · x1
[11#(x1)] = 1
[10#(x1)] = 1
the pairs
00#(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(10(x1)))))))))))))))))))) → 01#(10(01(10(00(01(11(10(00(00(00(00(00(01(11(11(10(x1))))))))))))))))) (489)
00#(00(00(00(00(01(10(00(01(10(01(10(01(11(11(11(10(01(11(11(x1)))))))))))))))))))) → 01#(10(01(10(00(01(11(10(00(00(00(00(00(01(11(11(11(x1))))))))))))))))) (507)
00#(01(10(01(10(00(01(11(10(01(10(01(10(00(00(01(11(11(10(01(x1)))))))))))))))))))) → 01#(10(01(x1))) (557)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 01#(10(01(10(01(11(10(01(10(01(10(00(00(00(00(00(x1)))))))))))))))) (562)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 01#(10(01(11(10(01(10(01(10(00(00(00(00(00(x1)))))))))))))) (564)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(00(x1)))))))))))))))))))) → 01#(10(01(10(00(00(00(00(00(x1))))))))) (569)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 01#(10(01(10(01(11(10(01(10(01(10(00(00(00(00(01(x1)))))))))))))))) (580)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 01#(10(01(11(10(01(10(01(10(00(00(00(00(01(x1)))))))))))))) (582)
00#(01(11(10(00(01(10(00(01(10(01(10(00(01(11(10(01(10(00(01(x1)))))))))))))))))))) → 01#(10(01(10(00(00(00(00(01(x1))))))))) (587)
00#(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(00(x1)))))))))))))))))))) → 01#(10(01(10(00(01(11(10(00(01(10(00(00(x1))))))))))))) (637)
00#(01(11(11(10(01(10(01(10(01(10(00(00(01(10(00(00(01(10(01(x1)))))))))))))))))))) → 01#(10(01(10(00(01(11(10(00(01(10(00(01(x1))))))))))))) (656)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(10(x1)))))))))))))))))))) → 01#(10(01(10(00(00(00(01(10(01(11(10(00(00(00(01(10(x1))))))))))))))))) (671)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(10(x1)))))))))))))))))))) → 01#(10(01(11(10(00(00(00(01(10(x1)))))))))) (678)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(11(x1)))))))))))))))))))) → 01#(10(01(10(00(00(00(01(10(01(11(10(00(00(00(01(11(x1))))))))))))))))) (689)
01#(11(11(10(00(01(10(00(00(01(10(01(10(00(00(00(01(10(01(11(x1)))))))))))))))))))) → 01#(10(01(11(10(00(00(00(01(11(x1)))))))))) (696)
11#(11(10(00(00(00(01(10(00(01(11(11(10(00(01(10(00(00(00(00(x1)))))))))))))))))))) → 01#(10(01(10(00(01(11(10(00(00(00(00(00(x1))))))))))))) (711)
11#(11(10(00(00(00(01(10(00(01(11(11(10(00(01(10(00(00(00(01(x1)))))))))))))))))))) → 01#(10(01(10(00(01(11(10(00(00(00(00(01(x1))))))))))))) (727)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(10(x1))))))))))))))))))))) → 01#(10(01(11(10(00(00(01(11(10(01(10(01(11(10(00(00(01(10(x1))))))))))))))))))) (738)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(10(x1))))))))))))))))))))) → 01#(10(01(11(10(00(00(01(10(x1))))))))) (748)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(11(x1))))))))))))))))))))) → 01#(10(01(11(10(00(00(01(11(10(01(10(01(11(10(00(00(01(11(x1))))))))))))))))))) (757)
10#(00(01(10(01(11(11(10(00(01(11(11(10(00(01(10(00(01(10(01(11(x1))))))))))))))))))))) → 01#(10(01(11(10(00(00(01(11(x1))))))))) (767)
could be deleted.

1.1.1.1.1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[00#(x1)] = 1 · x1
[00(x1)] = 1 · x1
[01(x1)] = 1 + 1 · x1
[10(x1)] = 1 · x1
[11(x1)] = 1 + 1 · x1
[01#(x1)] = 1 · x1
[11#(x1)] = 1 · x1
[10#(x1)] = 1 · x1
the pairs

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

could be deleted.

1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.