Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/29415)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
1(0(2(1(1(2(0(2(2(0(1(1(2(0(1(0(1(0(0(1(2(1(2(2(1(0(0(0(0(0(x1)))))))))))))))))))))))))))))) → 1(1(0(1(1(2(0(2(0(2(1(0(2(0(0(2(1(0(0(2(2(2(0(2(0(1(2(0(0(1(x1)))))))))))))))))))))))))))))) (100)
1(0(1(2(1(1(0(0(1(0(2(1(2(1(1(1(0(2(2(0(0(2(2(1(2(1(0(0(0(0(x1)))))))))))))))))))))))))))))) → 1(0(1(1(1(1(0(0(1(1(2(0(1(0(0(0(1(0(1(1(0(1(0(2(2(0(1(0(2(2(x1)))))))))))))))))))))))))))))) (101)
0(1(1(2(1(1(2(2(0(0(2(2(1(1(1(2(0(0(1(2(0(1(2(2(0(0(1(0(0(0(x1)))))))))))))))))))))))))))))) → 2(1(1(2(0(1(0(2(0(2(2(0(1(2(1(2(2(2(0(0(0(2(1(1(2(0(0(2(2(0(x1)))))))))))))))))))))))))))))) (102)
0(1(1(2(2(1(2(1(2(2(0(1(0(1(0(1(0(2(2(2(0(0(0(1(2(1(1(0(0(0(x1)))))))))))))))))))))))))))))) → 0(2(1(0(0(1(2(2(1(0(2(0(1(2(0(1(0(2(1(2(2(1(0(1(1(2(0(0(0(2(x1)))))))))))))))))))))))))))))) (103)
2(1(1(0(2(2(2(1(2(1(2(2(1(1(2(0(2(0(0(1(2(2(0(2(0(0(0(1(0(0(x1)))))))))))))))))))))))))))))) → 0(2(2(0(2(2(0(2(0(1(2(0(2(0(0(0(2(1(2(1(2(2(2(2(2(2(0(2(1(2(x1)))))))))))))))))))))))))))))) (104)
2(1(2(0(1(2(1(0(0(2(2(2(1(1(0(1(2(2(0(1(0(1(0(1(1(1(2(1(0(0(x1)))))))))))))))))))))))))))))) → 2(0(0(0(2(0(1(2(2(1(0(1(1(2(2(2(2(2(1(0(1(0(0(2(1(1(2(2(1(2(x1)))))))))))))))))))))))))))))) (105)
0(0(2(1(0(2(1(0(1(1(2(1(0(0(0(2(0(2(2(2(1(1(2(2(0(1(0(2(0(0(x1)))))))))))))))))))))))))))))) → 0(1(0(1(2(0(2(2(1(1(0(1(0(0(0(1(0(0(2(0(2(2(0(1(2(2(1(1(0(0(x1)))))))))))))))))))))))))))))) (106)
2(2(1(0(0(1(1(2(1(0(0(0(1(1(0(2(1(1(1(1(2(2(2(0(1(2(0(2(0(0(x1)))))))))))))))))))))))))))))) → 2(1(2(2(2(2(2(1(0(0(2(2(2(2(2(1(2(2(1(0(2(2(0(1(2(0(0(0(1(0(x1)))))))))))))))))))))))))))))) (107)
0(2(0(1(2(0(1(0(2(2(1(1(2(2(1(1(2(1(2(2(1(1(0(1(1(0(1(2(0(0(x1)))))))))))))))))))))))))))))) → 0(1(0(1(2(1(1(1(1(2(1(0(0(0(1(2(2(2(0(1(1(0(2(1(0(1(1(2(0(2(x1)))))))))))))))))))))))))))))) (108)
1(1(1(0(1(0(0(1(1(1(2(0(1(2(0(0(2(0(2(0(1(2(1(0(1(1(1(2(0(0(x1)))))))))))))))))))))))))))))) → 1(1(0(1(2(2(1(0(2(0(0(1(1(1(1(1(0(0(2(1(0(0(1(1(2(2(0(1(0(0(x1)))))))))))))))))))))))))))))) (109)
2(1(0(0(0(2(0(1(1(0(0(1(2(0(0(2(0(0(1(2(1(1(1(2(1(2(1(2(0(0(x1)))))))))))))))))))))))))))))) → 0(1(0(0(2(0(1(1(2(0(0(0(2(2(2(0(0(0(1(0(1(1(2(2(1(2(1(1(0(2(x1)))))))))))))))))))))))))))))) (110)
0(0(1(0(2(2(2(1(0(2(1(0(2(2(0(2(0(0(2(0(0(2(2(0(2(2(1(2(0(0(x1)))))))))))))))))))))))))))))) → 0(1(1(0(1(2(0(0(0(1(1(1(0(0(0(0(0(2(2(0(2(0(2(2(0(0(1(0(0(1(x1)))))))))))))))))))))))))))))) (111)
1(2(2(1(1(0(1(2(0(2(1(2(2(2(1(1(1(2(2(0(2(2(1(0(1(0(2(2(0(0(x1)))))))))))))))))))))))))))))) → 2(2(0(1(1(2(2(1(2(2(1(2(1(1(1(0(0(2(2(2(2(1(0(1(0(0(1(0(0(2(x1)))))))))))))))))))))))))))))) (112)
0(2(1(0(2(1(0(1(0(0(1(1(0(2(1(1(2(1(1(1(2(0(1(0(2(0(2(2(0(0(x1)))))))))))))))))))))))))))))) → 1(0(2(1(1(1(0(0(2(1(2(1(2(0(0(1(1(0(0(0(1(2(1(0(1(1(0(0(0(0(x1)))))))))))))))))))))))))))))) (113)
0(1(0(2(0(1(2(0(2(2(2(0(2(1(1(0(0(1(0(2(2(1(1(1(0(1(2(2(0(0(x1)))))))))))))))))))))))))))))) → 0(1(0(1(0(2(1(2(0(2(1(1(2(0(0(1(2(2(2(1(0(0(0(1(0(0(0(1(2(1(x1)))))))))))))))))))))))))))))) (114)
2(0(2(0(0(2(0(1(2(1(1(2(1(1(1(2(1(1(2(0(1(2(0(0(2(0(0(0(1(0(x1)))))))))))))))))))))))))))))) → 0(1(1(0(1(0(2(2(1(0(0(2(2(0(2(1(0(1(2(0(0(2(0(2(2(1(0(2(1(1(x1)))))))))))))))))))))))))))))) (115)
1(1(2(0(0(1(2(1(1(2(0(0(2(1(1(0(2(1(2(2(0(2(2(0(0(1(0(0(1(0(x1)))))))))))))))))))))))))))))) → 0(2(0(0(2(2(0(1(1(0(0(1(2(1(0(0(0(1(2(2(1(2(0(0(0(1(2(1(1(2(x1)))))))))))))))))))))))))))))) (116)
1(1(2(0(0(1(0(0(1(1(1(1(0(2(0(1(2(0(0(1(2(0(2(1(1(0(2(0(1(0(x1)))))))))))))))))))))))))))))) → 2(2(2(2(1(0(2(0(2(2(1(0(2(0(1(0(1(2(1(0(0(0(0(1(0(2(1(2(1(0(x1)))))))))))))))))))))))))))))) (117)
2(0(1(0(0(1(2(0(1(1(0(2(0(2(1(2(0(1(1(1(0(2(0(2(0(0(1(1(1(0(x1)))))))))))))))))))))))))))))) → 1(2(2(2(2(1(0(1(0(1(0(2(0(0(0(0(2(2(2(2(0(1(0(2(1(0(1(0(0(1(x1)))))))))))))))))))))))))))))) (118)
0(2(1(1(1(0(2(2(2(2(0(2(2(1(1(1(0(1(2(1(1(1(0(1(2(1(1(1(1(0(x1)))))))))))))))))))))))))))))) → 1(1(2(2(1(2(2(0(2(0(2(1(1(1(0(1(2(2(1(1(0(1(0(0(2(0(1(1(2(1(x1)))))))))))))))))))))))))))))) (119)
0(0(1(1(2(2(1(0(0(1(1(2(0(2(2(1(2(1(2(1(0(0(0(2(1(2(2(1(1(0(x1)))))))))))))))))))))))))))))) → 0(1(1(2(0(2(0(0(1(2(0(1(2(2(2(0(0(2(2(1(1(0(1(0(2(1(1(1(0(1(x1)))))))))))))))))))))))))))))) (120)
0(0(1(0(1(2(1(1(0(0(2(2(1(2(2(1(2(2(2(2(2(0(2(0(1(0(0(2(1(0(x1)))))))))))))))))))))))))))))) → 2(2(1(2(0(1(2(0(2(0(0(0(0(1(2(1(0(2(2(2(2(1(2(2(0(2(0(0(1(2(x1)))))))))))))))))))))))))))))) (121)
2(2(2(2(1(1(2(0(1(0(1(1(1(2(0(1(0(1(2(0(1(2(0(2(2(1(0(2(1(0(x1)))))))))))))))))))))))))))))) → 0(1(1(1(1(2(1(0(2(1(1(2(0(1(1(0(2(2(0(2(1(0(0(2(2(0(2(2(2(2(x1)))))))))))))))))))))))))))))) (122)
0(1(2(1(2(0(1(2(2(1(1(2(2(1(1(2(1(2(2(0(1(0(0(2(0(2(2(2(1(0(x1)))))))))))))))))))))))))))))) → 0(0(2(1(0(2(0(2(1(2(1(1(1(2(1(1(1(2(1(0(1(1(1(0(2(2(0(1(0(0(x1)))))))))))))))))))))))))))))) (123)
0(2(2(2(0(1(0(1(0(2(2(1(2(2(1(0(1(0(2(1(0(0(0(1(1(2(2(2(1(0(x1)))))))))))))))))))))))))))))) → 1(2(0(2(1(2(2(0(2(1(1(0(2(0(2(2(2(1(0(2(0(0(2(1(0(0(1(0(2(0(x1)))))))))))))))))))))))))))))) (124)
1(0(1(2(0(1(0(0(0(0(0(1(1(1(1(2(1(0(2(2(0(2(1(0(1(2(0(1(2(0(x1)))))))))))))))))))))))))))))) → 2(0(0(0(2(1(0(1(2(0(0(0(1(2(2(2(0(2(2(1(2(0(0(1(2(2(0(0(1(1(x1)))))))))))))))))))))))))))))) (125)
1(1(2(0(0(1(2(1(2(2(0(2(1(1(1(1(0(0(0(2(0(2(2(0(1(0(2(1(2(0(x1)))))))))))))))))))))))))))))) → 1(2(0(1(0(1(0(2(2(1(0(1(0(0(2(0(1(1(2(2(0(2(0(2(1(2(2(2(0(1(x1)))))))))))))))))))))))))))))) (126)
1(1(2(0(2(2(1(1(1(2(2(0(0(1(1(1(1(1(0(0(1(0(1(1(1(0(2(1(2(0(x1)))))))))))))))))))))))))))))) → 1(1(1(1(1(0(0(2(2(1(2(1(0(0(0(2(1(1(1(0(2(1(1(2(1(0(1(0(1(2(x1)))))))))))))))))))))))))))))) (127)
2(2(1(1(1(0(2(1(1(2(1(0(0(1(2(2(0(1(0(0(1(1(0(1(0(0(1(2(2(0(x1)))))))))))))))))))))))))))))) → 1(1(0(1(2(2(1(0(0(2(0(2(2(1(2(1(1(0(0(2(0(2(1(1(2(0(0(2(0(2(x1)))))))))))))))))))))))))))))) (128)
2(0(2(0(1(1(0(0(0(1(1(2(2(1(0(1(0(2(1(2(0(2(2(0(2(1(1(2(2(0(x1)))))))))))))))))))))))))))))) → 2(2(1(0(1(1(0(1(1(1(1(1(1(0(2(0(1(0(0(0(2(2(2(0(2(0(1(2(0(0(x1)))))))))))))))))))))))))))))) (129)
1(0(0(1(1(2(2(2(2(2(0(1(0(0(2(2(2(0(2(1(0(0(2(0(2(0(2(2(2(0(x1)))))))))))))))))))))))))))))) → 2(1(1(1(0(0(1(2(0(0(2(1(0(0(1(2(2(0(2(0(2(0(0(2(0(2(2(0(1(0(x1)))))))))))))))))))))))))))))) (130)
2(1(2(1(0(0(1(1(2(2(0(2(1(2(2(0(1(0(1(2(2(1(1(0(1(0(0(0(0(1(x1)))))))))))))))))))))))))))))) → 1(2(2(1(0(0(2(0(1(2(1(0(0(0(2(2(0(1(0(1(0(2(1(0(1(1(1(2(0(2(x1)))))))))))))))))))))))))))))) (131)
0(0(1(1(2(0(1(0(1(1(0(2(1(0(1(2(2(2(0(2(1(1(2(2(1(0(0(0(0(1(x1)))))))))))))))))))))))))))))) → 1(0(1(0(2(0(2(2(2(0(1(1(2(0(0(2(2(1(0(1(0(2(0(2(0(2(2(0(2(2(x1)))))))))))))))))))))))))))))) (132)
0(2(2(2(0(2(0(0(2(0(0(2(1(0(1(0(1(1(2(1(0(1(2(2(1(1(1(0(0(1(x1)))))))))))))))))))))))))))))) → 0(0(2(0(2(1(1(2(0(0(2(1(2(2(2(0(2(1(2(0(1(1(1(0(0(1(2(0(2(0(x1)))))))))))))))))))))))))))))) (133)
1(2(1(1(1(2(0(0(0(0(1(2(0(1(2(2(0(2(2(1(2(2(1(0(0(1(2(0(0(1(x1)))))))))))))))))))))))))))))) → 2(2(1(2(0(2(0(1(2(1(2(0(2(2(1(2(2(0(0(2(0(0(1(0(1(0(2(1(0(2(x1)))))))))))))))))))))))))))))) (134)
2(2(1(0(0(1(2(2(1(1(0(0(0(1(0(1(1(0(2(2(1(1(1(2(0(1(2(0(0(1(x1)))))))))))))))))))))))))))))) → 2(0(2(1(1(2(2(2(1(0(1(2(0(0(2(1(1(2(2(0(0(0(0(0(1(2(2(2(1(1(x1)))))))))))))))))))))))))))))) (135)
1(0(0(2(1(0(1(0(2(2(2(2(2(2(1(1(0(1(1(0(2(1(1(0(0(2(0(1(0(1(x1)))))))))))))))))))))))))))))) → 1(1(2(2(2(2(2(0(0(0(1(2(0(2(1(0(0(2(2(0(2(2(0(1(1(0(1(2(2(2(x1)))))))))))))))))))))))))))))) (136)
0(0(2(0(2(2(2(2(2(1(0(2(0(2(2(1(2(2(0(1(1(1(1(1(0(0(2(1(0(1(x1)))))))))))))))))))))))))))))) → 0(1(2(0(0(1(1(2(0(1(1(2(2(1(2(0(1(1(2(0(2(0(2(2(0(0(0(1(2(1(x1)))))))))))))))))))))))))))))) (137)
2(0(1(0(1(2(1(2(0(1(0(0(1(1(2(2(2(2(1(0(2(2(1(0(1(0(2(1(0(1(x1)))))))))))))))))))))))))))))) → 2(1(1(0(1(2(1(1(2(0(2(0(1(0(0(1(1(0(2(0(1(0(2(1(0(0(1(2(1(1(x1)))))))))))))))))))))))))))))) (138)
0(1(1(1(2(2(2(2(2(1(1(2(1(2(0(0(0(2(2(1(2(2(0(1(2(1(2(1(0(1(x1)))))))))))))))))))))))))))))) → 1(0(0(1(1(0(2(1(0(1(1(1(1(1(0(0(2(0(2(2(1(0(1(2(2(1(1(1(2(0(x1)))))))))))))))))))))))))))))) (139)
0(2(1(0(0(2(2(1(2(0(1(0(1(1(1(2(2(0(0(2(1(0(0(0(1(2(2(1(0(1(x1)))))))))))))))))))))))))))))) → 2(0(0(0(2(1(0(0(1(2(2(2(2(1(2(0(0(2(2(0(2(2(0(0(1(0(1(1(1(2(x1)))))))))))))))))))))))))))))) (140)
0(1(2(2(2(1(2(2(2(1(0(1(1(2(2(1(0(2(2(2(0(2(2(0(2(1(0(2(0(1(x1)))))))))))))))))))))))))))))) → 1(1(2(1(0(1(1(1(2(2(0(2(2(2(1(1(0(0(1(0(0(2(2(0(0(0(1(0(1(1(x1)))))))))))))))))))))))))))))) (141)
1(1(1(0(1(2(0(1(1(2(0(2(2(1(1(1(0(0(1(2(0(0(0(1(0(1(1(2(0(1(x1)))))))))))))))))))))))))))))) → 1(1(1(0(2(2(2(0(2(1(0(0(2(0(2(1(2(1(0(1(1(0(0(1(2(2(1(2(1(0(x1)))))))))))))))))))))))))))))) (142)
2(1(2(2(1(2(0(2(2(1(1(1(1(0(2(1(0(1(1(1(0(0(0(1(2(2(1(2(0(1(x1)))))))))))))))))))))))))))))) → 1(1(0(1(1(0(0(1(2(0(1(2(0(0(0(2(2(1(2(1(1(1(2(1(2(0(2(1(2(2(x1)))))))))))))))))))))))))))))) (143)
0(1(0(2(1(2(2(2(2(0(0(2(1(2(2(2(2(2(1(0(0(0(2(0(0(1(2(2(0(1(x1)))))))))))))))))))))))))))))) → 1(0(0(2(0(2(2(0(1(2(2(1(0(0(1(0(2(1(2(0(1(0(2(1(0(2(2(0(2(0(x1)))))))))))))))))))))))))))))) (144)
2(0(0(1(1(0(1(1(2(1(0(2(1(0(1(0(2(0(0(0(0(0(2(2(1(2(2(2(0(1(x1)))))))))))))))))))))))))))))) → 2(0(1(1(0(0(1(0(1(1(0(0(2(0(0(2(0(1(2(1(0(1(2(2(2(2(2(0(0(2(x1)))))))))))))))))))))))))))))) (145)
1(2(1(2(0(1(1(1(2(1(0(0(1(2(1(0(2(1(2(1(2(2(1(2(1(1(0(0(1(1(x1)))))))))))))))))))))))))))))) → 2(2(1(2(1(0(1(0(1(1(2(2(1(0(2(1(1(1(2(0(1(1(2(0(1(1(0(0(1(1(x1)))))))))))))))))))))))))))))) (146)
2(0(2(0(1(1(1(2(0(2(1(1(2(2(1(0(1(0(0(2(2(0(0(1(1(2(0(0(1(1(x1)))))))))))))))))))))))))))))) → 1(2(1(0(1(0(1(2(0(0(2(1(2(1(2(1(0(0(2(1(0(0(1(0(0(1(0(1(2(2(x1)))))))))))))))))))))))))))))) (147)
0(0(0(2(1(2(0(0(2(1(2(1(0(2(2(2(0(0(1(1(1(2(1(2(0(0(1(0(1(1(x1)))))))))))))))))))))))))))))) → 0(0(2(2(2(2(2(1(0(1(0(0(2(2(2(1(0(2(0(0(1(2(0(1(1(1(1(0(1(0(x1)))))))))))))))))))))))))))))) (148)
0(1(0(0(0(0(0(0(1(1(1(2(0(0(0(1(2(0(2(1(1(0(0(1(1(2(1(0(1(1(x1)))))))))))))))))))))))))))))) → 1(0(1(1(0(0(2(0(1(0(1(2(2(1(0(2(2(2(0(0(1(0(0(0(1(0(2(0(1(0(x1)))))))))))))))))))))))))))))) (149)
0(1(0(0(1(0(1(2(0(1(2(1(1(2(1(1(2(0(1(1(1(0(2(2(2(1(2(0(1(1(x1)))))))))))))))))))))))))))))) → 2(0(0(2(1(2(2(1(0(1(2(2(1(2(2(2(2(1(2(1(1(0(0(0(0(0(0(1(0(2(x1)))))))))))))))))))))))))))))) (150)
0(0(0(0(2(1(1(2(1(1(0(2(0(1(0(1(1(2(0(1(0(1(2(2(1(0(0(1(1(1(x1)))))))))))))))))))))))))))))) → 1(2(0(1(2(2(2(0(0(1(0(0(0(2(0(1(1(0(1(1(2(1(0(0(1(1(2(0(0(2(x1)))))))))))))))))))))))))))))) (151)
2(0(0(2(1(1(1(1(1(2(2(0(0(2(2(0(0(0(2(2(1(2(0(0(0(0(2(1(1(1(x1)))))))))))))))))))))))))))))) → 2(0(0(1(0(2(1(1(1(0(1(0(2(1(1(0(0(1(0(1(2(2(0(1(1(2(0(2(0(0(x1)))))))))))))))))))))))))))))) (152)
2(2(2(0(2(2(0(0(2(2(0(0(2(1(0(0(2(2(1(2(2(0(1(1(0(1(2(1(1(1(x1)))))))))))))))))))))))))))))) → 2(2(1(1(2(1(0(1(0(0(2(0(0(2(0(2(1(2(0(2(2(2(2(0(0(2(1(1(2(1(x1)))))))))))))))))))))))))))))) (153)
2(1(0(0(2(1(0(0(1(0(0(0(1(0(1(1(1(2(1(1(2(2(0(1(1(2(2(1(1(1(x1)))))))))))))))))))))))))))))) → 1(1(2(2(1(1(0(1(0(1(2(0(0(2(2(0(0(1(1(0(0(0(1(1(2(1(1(0(1(1(x1)))))))))))))))))))))))))))))) (154)
0(1(2(2(0(1(2(0(0(2(1(2(2(0(0(1(1(2(1(1(1(0(2(2(0(1(0(2(1(1(x1)))))))))))))))))))))))))))))) → 1(2(0(0(1(0(0(1(0(2(1(1(1(1(1(2(1(0(0(0(1(2(2(1(2(0(0(0(1(2(x1)))))))))))))))))))))))))))))) (155)
0(1(0(0(1(0(0(0(1(1(1(0(2(1(1(2(1(1(0(2(2(0(0(2(1(2(0(2(1(1(x1)))))))))))))))))))))))))))))) → 1(0(0(0(0(0(2(0(0(2(1(2(2(2(1(0(1(1(2(1(2(0(1(1(2(2(2(0(0(2(x1)))))))))))))))))))))))))))))) (156)
0(0(1(2(0(1(1(1(0(0(2(2(0(2(2(0(0(1(1(0(1(1(2(0(2(2(0(2(1(1(x1)))))))))))))))))))))))))))))) → 1(0(1(1(1(1(1(0(2(1(0(2(0(1(0(0(0(2(0(0(0(0(2(1(0(1(2(0(2(2(x1)))))))))))))))))))))))))))))) (157)
0(0(1(1(0(0(1(2(1(0(0(2(1(1(1(2(2(2(0(1(1(0(0(1(2(1(1(2(1(1(x1)))))))))))))))))))))))))))))) → 2(0(0(1(2(2(1(0(2(2(1(0(0(0(1(2(2(2(2(0(1(0(2(2(1(1(1(1(2(2(x1)))))))))))))))))))))))))))))) (158)
1(2(2(2(0(1(0(1(1(1(0(1(0(0(0(2(2(1(2(0(0(0(1(1(2(0(2(2(1(1(x1)))))))))))))))))))))))))))))) → 2(1(0(0(1(1(0(2(0(2(0(2(0(2(1(1(1(2(2(2(1(0(2(0(2(1(0(2(0(1(x1)))))))))))))))))))))))))))))) (159)
2(2(1(1(1(0(2(0(1(2(0(0(2(0(0(1(1(2(0(0(2(2(2(0(0(0(1(0(2(1(x1)))))))))))))))))))))))))))))) → 2(1(0(0(2(2(0(1(0(1(1(0(1(0(1(0(1(0(0(0(0(1(0(0(2(2(2(1(1(2(x1)))))))))))))))))))))))))))))) (160)
1(2(1(2(0(1(0(2(2(2(0(1(0(2(2(1(0(1(2(2(0(2(0(2(1(0(2(0(2(1(x1)))))))))))))))))))))))))))))) → 0(2(0(0(2(0(2(0(2(1(1(1(1(0(2(0(1(2(2(0(0(1(1(1(2(0(0(1(1(0(x1)))))))))))))))))))))))))))))) (161)
1(1(0(2(0(2(1(2(1(2(1(0(1(1(2(2(2(0(0(1(2(1(0(2(1(0(0(1(2(1(x1)))))))))))))))))))))))))))))) → 1(1(0(2(0(1(1(2(2(1(0(1(0(2(2(0(1(0(2(1(2(2(1(1(0(2(2(2(1(0(x1)))))))))))))))))))))))))))))) (162)
2(1(0(2(2(0(0(1(0(0(2(1(2(0(2(2(0(1(0(0(2(0(0(0(1(1(0(1(2(1(x1)))))))))))))))))))))))))))))) → 2(0(0(0(0(2(0(1(2(2(0(1(1(1(2(2(1(2(2(0(0(0(0(0(1(2(0(2(0(2(x1)))))))))))))))))))))))))))))) (163)
0(0(1(1(2(0(2(0(1(0(1(1(0(2(0(0(1(1(0(0(0(1(1(1(0(1(2(1(2(1(x1)))))))))))))))))))))))))))))) → 2(1(1(0(0(1(2(1(0(2(0(0(1(2(0(2(2(1(0(1(1(0(2(2(2(0(0(2(0(2(x1)))))))))))))))))))))))))))))) (164)
2(2(0(1(2(2(0(0(1(0(1(2(1(1(0(2(0(1(2(1(0(2(0(1(2(2(2(1(2(1(x1)))))))))))))))))))))))))))))) → 2(1(0(2(1(0(2(1(2(2(2(0(0(2(0(0(1(0(1(2(1(2(2(1(0(1(2(1(2(1(x1)))))))))))))))))))))))))))))) (165)
2(1(0(2(1(1(2(2(2(0(1(2(0(2(1(1(0(2(1(2(2(2(1(0(0(0(0(2(2(1(x1)))))))))))))))))))))))))))))) → 2(1(2(2(0(2(0(0(2(1(0(0(2(1(1(1(1(2(1(1(2(0(2(0(2(1(0(1(0(2(x1)))))))))))))))))))))))))))))) (166)
2(2(0(0(2(2(1(2(1(0(0(1(0(2(1(2(2(1(1(0(2(1(2(2(1(0(0(2(2(1(x1)))))))))))))))))))))))))))))) → 2(0(2(1(1(2(0(0(1(1(1(2(0(0(1(1(0(1(1(2(0(2(0(0(2(1(1(0(1(2(x1)))))))))))))))))))))))))))))) (167)
0(0(2(1(2(2(0(2(2(1(2(0(2(2(2(1(2(0(2(2(2(0(0(0(2(2(0(2(2(1(x1)))))))))))))))))))))))))))))) → 0(2(1(2(1(2(2(0(1(2(0(1(0(2(0(2(1(1(0(0(0(1(0(2(0(0(1(1(1(0(x1)))))))))))))))))))))))))))))) (168)
0(0(2(0(2(1(1(1(0(1(1(2(2(1(2(2(2(2(0(0(1(0(2(1(1(0(1(2(2(1(x1)))))))))))))))))))))))))))))) → 0(0(2(1(1(0(0(0(2(1(2(2(0(2(1(0(2(1(1(0(1(2(0(2(1(1(1(1(1(1(x1)))))))))))))))))))))))))))))) (169)
0(0(2(1(2(2(0(1(1(1(1(2(0(0(2(1(0(0(2(2(2(0(1(1(2(1(2(2(2(1(x1)))))))))))))))))))))))))))))) → 0(2(1(2(0(2(1(1(1(0(1(2(2(2(0(1(0(1(0(0(0(2(0(2(1(1(2(1(1(2(x1)))))))))))))))))))))))))))))) (170)
1(0(0(0(1(2(2(2(0(1(1(1(2(2(1(0(2(0(2(0(0(0(1(2(2(1(2(2(2(1(x1)))))))))))))))))))))))))))))) → 0(0(2(0(2(0(2(2(0(0(2(1(0(0(1(1(1(2(1(0(1(0(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))))) (171)
0(0(0(2(2(1(1(2(1(1(2(1(0(0(2(0(2(0(0(1(0(0(2(0(1(0(0(0(0(2(x1)))))))))))))))))))))))))))))) → 0(2(0(0(2(0(0(2(1(2(0(1(0(2(0(1(2(0(0(0(0(0(1(2(0(0(1(2(1(2(x1)))))))))))))))))))))))))))))) (172)
0(1(1(2(2(2(1(0(0(1(2(0(2(2(2(1(1(1(1(2(0(1(0(0(2(1(0(0(0(2(x1)))))))))))))))))))))))))))))) → 0(1(0(0(2(1(1(1(1(0(0(2(2(0(1(2(1(2(2(2(2(0(0(1(2(0(1(1(0(2(x1)))))))))))))))))))))))))))))) (173)
0(1(2(1(1(2(0(1(2(0(0(2(0(2(2(1(0(2(2(2(2(0(1(0(2(1(0(1(0(2(x1)))))))))))))))))))))))))))))) → 1(1(1(2(0(0(0(1(2(1(1(0(2(0(1(2(1(0(0(0(2(0(0(1(2(1(0(0(0(1(x1)))))))))))))))))))))))))))))) (174)
2(0(1(1(0(0(0(1(2(0(0(0(1(2(2(2(1(1(1(0(0(0(1(1(1(0(1(1(0(2(x1)))))))))))))))))))))))))))))) → 1(0(1(2(1(1(0(1(0(1(0(0(0(0(2(2(0(0(2(2(0(1(1(2(2(1(0(0(1(2(x1)))))))))))))))))))))))))))))) (175)
2(0(0(0(1(2(1(1(2(1(2(1(2(1(0(0(1(2(0(2(1(2(0(1(2(0(1(1(0(2(x1)))))))))))))))))))))))))))))) → 0(0(1(0(1(1(2(2(1(1(2(2(1(2(0(1(0(0(0(2(1(0(0(1(1(2(1(2(1(0(x1)))))))))))))))))))))))))))))) (176)
1(2(0(0(0(1(2(2(1(1(1(2(0(0(1(1(2(2(2(2(2(2(2(0(2(1(1(1(0(2(x1)))))))))))))))))))))))))))))) → 2(1(2(1(1(0(0(1(2(1(1(1(0(1(2(1(2(2(1(0(2(1(0(2(0(0(0(0(2(1(x1)))))))))))))))))))))))))))))) (177)
0(1(1(0(1(0(1(0(0(0(2(0(0(2(0(2(2(2(1(2(1(0(2(1(0(1(2(1(0(2(x1)))))))))))))))))))))))))))))) → 1(1(0(0(2(2(0(1(0(1(2(0(0(1(1(2(0(0(0(0(0(2(2(1(2(2(0(1(0(2(x1)))))))))))))))))))))))))))))) (178)
2(1(1(0(1(1(1(2(0(0(0(0(1(1(2(0(1(2(1(2(1(0(2(1(1(2(0(2(0(2(x1)))))))))))))))))))))))))))))) → 1(1(1(2(0(2(2(0(2(0(1(0(1(0(0(1(1(1(1(0(2(1(0(2(2(2(1(1(0(0(x1)))))))))))))))))))))))))))))) (179)
2(2(2(0(1(2(0(1(0(2(1(0(0(0(2(0(2(2(0(2(1(1(1(0(1(1(1(2(0(2(x1)))))))))))))))))))))))))))))) → 0(2(2(1(2(0(0(2(1(1(0(1(1(1(1(0(2(2(2(1(2(0(2(1(0(0(1(0(0(0(x1)))))))))))))))))))))))))))))) (180)
0(0(0(2(0(1(1(2(0(2(1(2(2(1(0(1(1(0(1(0(2(1(2(2(1(2(1(2(0(2(x1)))))))))))))))))))))))))))))) → 1(0(1(2(0(0(2(1(2(0(2(1(0(2(0(2(0(1(0(2(0(1(2(1(1(2(2(2(0(2(x1)))))))))))))))))))))))))))))) (181)
1(0(0(1(0(2(1(1(1(1(1(2(2(2(1(0(1(2(1(2(2(0(1(0(2(2(2(2(0(2(x1)))))))))))))))))))))))))))))) → 1(2(1(1(2(0(2(1(1(2(1(0(1(1(2(0(0(2(1(1(0(1(0(1(2(2(0(1(2(0(x1)))))))))))))))))))))))))))))) (182)
0(2(2(2(1(2(1(0(1(2(1(1(0(0(1(2(0(0(2(0(1(2(2(2(1(2(0(0(1(2(x1)))))))))))))))))))))))))))))) → 0(2(1(1(0(2(0(2(1(1(1(2(0(1(0(0(1(2(2(0(0(1(2(2(0(0(1(2(2(1(x1)))))))))))))))))))))))))))))) (183)
0(1(0(1(2(2(0(1(1(1(2(0(0(0(1(2(1(2(0(0(1(1(2(0(0(0(1(0(1(2(x1)))))))))))))))))))))))))))))) → 0(0(0(1(2(0(2(0(1(1(1(0(1(1(2(0(1(2(1(1(0(0(2(0(1(0(1(1(0(0(x1)))))))))))))))))))))))))))))) (184)
2(1(1(2(0(0(0(2(1(1(0(2(0(0(0(1(0(0(1(2(1(0(0(2(1(1(1(0(1(2(x1)))))))))))))))))))))))))))))) → 1(2(1(0(1(0(1(0(0(2(0(1(2(0(2(2(2(2(0(0(0(0(2(1(1(0(1(0(1(2(x1)))))))))))))))))))))))))))))) (185)
0(0(1(1(0(2(2(2(1(2(0(1(2(2(1(2(2(2(1(2(0(0(0(2(0(2(1(0(1(2(x1)))))))))))))))))))))))))))))) → 0(2(1(1(1(1(1(0(0(2(0(2(2(2(1(2(0(0(1(0(1(1(1(1(0(1(0(0(0(2(x1)))))))))))))))))))))))))))))) (186)
0(0(2(0(2(2(2(0(1(2(1(1(0(2(2(2(2(0(2(2(2(0(0(0(1(2(2(0(1(2(x1)))))))))))))))))))))))))))))) → 2(0(2(0(1(0(2(0(0(1(2(2(0(1(0(1(2(1(0(1(1(2(0(0(0(2(2(1(0(2(x1)))))))))))))))))))))))))))))) (187)
0(1(2(0(2(0(0(2(1(2(1(2(1(2(2(0(2(1(1(0(2(1(2(0(1(2(2(0(1(2(x1)))))))))))))))))))))))))))))) → 1(2(0(0(1(1(2(0(2(0(0(1(0(0(2(0(1(1(1(2(1(2(0(1(1(2(0(1(0(1(x1)))))))))))))))))))))))))))))) (188)
1(1(2(0(2(0(0(1(1(2(1(0(1(0(2(2(2(2(2(2(2(2(0(0(1(1(1(1(1(2(x1)))))))))))))))))))))))))))))) → 1(2(1(0(2(1(0(0(1(1(1(2(1(0(1(0(0(1(1(2(1(0(2(2(2(1(1(1(0(2(x1)))))))))))))))))))))))))))))) (189)
0(1(0(1(1(2(0(0(0(0(2(1(1(0(0(0(1(0(0(1(2(1(0(2(2(0(2(1(1(2(x1)))))))))))))))))))))))))))))) → 0(0(2(0(2(1(1(0(2(0(1(0(0(1(1(1(0(2(0(1(2(0(0(0(0(1(0(2(1(1(x1)))))))))))))))))))))))))))))) (190)
2(0(0(2(0(1(2(1(2(2(2(2(0(1(1(1(0(2(2(0(2(0(2(0(0(0(1(2(1(2(x1)))))))))))))))))))))))))))))) → 1(1(1(0(0(1(2(0(2(2(0(2(1(1(0(1(0(0(0(1(1(0(1(0(0(1(0(1(2(0(x1)))))))))))))))))))))))))))))) (191)
0(1(1(2(1(0(0(2(1(1(2(2(0(2(1(2(2(2(2(2(1(2(1(0(2(0(2(0(2(2(x1)))))))))))))))))))))))))))))) → 1(1(2(1(1(1(2(2(0(1(0(0(1(1(2(0(2(1(1(0(1(2(0(1(0(0(2(0(2(0(x1)))))))))))))))))))))))))))))) (192)
2(1(0(2(1(0(0(0(0(2(0(2(2(2(1(1(1(1(2(0(0(0(0(2(2(2(2(0(2(2(x1)))))))))))))))))))))))))))))) → 0(0(1(0(0(0(0(1(1(0(1(2(1(0(2(1(2(2(0(2(0(2(2(1(1(0(0(1(1(0(x1)))))))))))))))))))))))))))))) (193)
2(1(0(1(1(0(0(0(2(1(2(2(1(2(2(2(0(2(1(0(1(1(2(1(1(0(0(1(2(2(x1)))))))))))))))))))))))))))))) → 0(1(1(0(2(0(1(2(0(1(2(1(1(2(2(2(2(2(1(0(1(0(1(0(0(2(1(1(0(1(x1)))))))))))))))))))))))))))))) (194)
0(2(1(1(1(0(2(2(1(1(2(0(2(2(1(1(0(1(0(0(0(2(0(2(1(2(0(1(2(2(x1)))))))))))))))))))))))))))))) → 0(1(1(2(0(1(0(0(1(2(2(0(1(0(2(2(0(1(0(0(1(1(1(0(1(1(0(2(1(1(x1)))))))))))))))))))))))))))))) (195)
1(0(0(1(1(2(0(1(1(1(2(2(1(1(2(0(1(0(0(2(2(1(0(0(1(0(1(1(2(2(x1)))))))))))))))))))))))))))))) → 0(1(2(1(1(2(0(0(1(0(1(1(0(1(0(0(0(0(2(1(0(2(1(1(1(1(2(1(0(1(x1)))))))))))))))))))))))))))))) (196)
2(2(2(1(1(0(2(0(1(1(1(0(0(0(2(2(1(0(1(0(0(1(1(0(2(0(2(1(2(2(x1)))))))))))))))))))))))))))))) → 1(0(2(2(2(2(0(1(0(0(1(1(2(0(1(2(1(2(0(1(2(1(0(1(0(1(2(0(0(0(x1)))))))))))))))))))))))))))))) (197)
2(0(0(0(1(1(2(2(1(1(0(1(2(2(0(0(2(2(0(1(0(2(2(1(2(2(1(2(2(2(x1)))))))))))))))))))))))))))))) → 1(0(2(0(0(2(0(0(2(0(1(0(2(1(2(1(0(0(1(1(0(1(2(1(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))) (198)

1.1 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐), 2(☐)}

We obtain the transformed TRS

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

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[10(x1)] = 1 · x1 + 38
[02(x1)] = 1 · x1 + 16
[21(x1)] = 1 · x1 + 12
[11(x1)] = 1 · x1 + 41
[12(x1)] = 1 · x1 + 59
[20(x1)] = 1 · x1 + 10
[22(x1)] = 1 · x1 + 29
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
all of the following rules can be deleted.

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

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[22(x1)] = 1 · x1 + 2
[21(x1)] = 1 · x1
[10(x1)] = 1 · x1 + 4
[00(x1)] = 1 · x1 + 1
[01(x1)] = 1 · x1
[11(x1)] = 1 · x1 + 2
[12(x1)] = 1 · x1 + 1
[02(x1)] = 1 · x1 + 5
[20(x1)] = 1 · x1 + 3
all of the following rules can be deleted.
11(12(20(02(22(21(11(11(12(22(20(00(01(11(11(11(11(10(00(01(10(01(11(11(10(02(21(12(20(02(x1)))))))))))))))))))))))))))))) → 11(11(11(11(10(00(02(22(21(12(21(10(00(00(02(21(11(11(10(02(21(11(12(21(10(01(10(01(12(22(x1)))))))))))))))))))))))))))))) (408)
10(00(01(10(02(21(11(11(11(11(12(22(22(21(10(01(12(21(12(22(20(01(10(02(22(22(22(20(02(20(x1)))))))))))))))))))))))))))))) → 12(21(11(12(20(02(21(11(12(21(10(01(11(12(20(00(02(21(11(10(01(10(01(12(22(20(01(12(20(00(x1)))))))))))))))))))))))))))))) (476)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[22(x1)] = 1 · x1 + 1
[21(x1)] = 1 · x1 + 4
[10(x1)] = 1 · x1
[00(x1)] = 1 · x1
[01(x1)] = 1 · x1
[11(x1)] = 1 · x1 + 11
[12(x1)] = 1 · x1 + 5
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
all of the following rules can be deleted.
22(21(10(00(01(11(12(21(10(00(00(01(11(10(02(21(11(11(11(12(22(22(20(01(12(20(02(20(00(01(x1)))))))))))))))))))))))))))))) → 21(12(22(22(22(22(21(10(00(02(22(22(22(22(21(12(22(21(10(02(22(20(01(12(20(00(00(01(10(01(x1)))))))))))))))))))))))))))))) (382)
22(21(10(00(01(11(12(21(10(00(00(01(11(10(02(21(11(11(11(12(22(22(20(01(12(20(02(20(00(00(x1)))))))))))))))))))))))))))))) → 21(12(22(22(22(22(21(10(00(02(22(22(22(22(21(12(22(21(10(02(22(20(01(12(20(00(00(01(10(00(x1)))))))))))))))))))))))))))))) (383)
22(21(10(00(01(11(12(21(10(00(00(01(11(10(02(21(11(11(11(12(22(22(20(01(12(20(02(20(00(02(x1)))))))))))))))))))))))))))))) → 21(12(22(22(22(22(21(10(00(02(22(22(22(22(21(12(22(21(10(02(22(20(01(12(20(00(00(01(10(02(x1)))))))))))))))))))))))))))))) (384)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[22(x1)] = 1 · x1
[21(x1)] = 1 · x1
[10(x1)] = 1 · x1
[00(x1)] = 1 · x1 + 2
[01(x1)] = 1 · x1 + 1
[12(x1)] = 1 · x1
[11(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
all of the following rules can be deleted.
22(21(10(00(01(12(22(21(11(10(00(00(01(10(01(11(10(02(22(21(11(11(12(20(01(12(20(00(01(11(x1)))))))))))))))))))))))))))))) → 20(02(21(11(12(22(22(21(10(01(12(20(00(02(21(11(12(22(20(00(00(00(00(01(12(22(22(21(11(11(x1)))))))))))))))))))))))))))))) (415)
22(21(10(00(01(12(22(21(11(10(00(00(01(10(01(11(10(02(22(21(11(11(12(20(01(12(20(00(01(10(x1)))))))))))))))))))))))))))))) → 20(02(21(11(12(22(22(21(10(01(12(20(00(02(21(11(12(22(20(00(00(00(00(01(12(22(22(21(11(10(x1)))))))))))))))))))))))))))))) (416)
22(21(10(00(01(12(22(21(11(10(00(00(01(10(01(11(10(02(22(21(11(11(12(20(01(12(20(00(01(12(x1)))))))))))))))))))))))))))))) → 20(02(21(11(12(22(22(21(10(01(12(20(00(02(21(11(12(22(20(00(00(00(00(01(12(22(22(21(11(12(x1)))))))))))))))))))))))))))))) (417)
22(22(20(02(22(20(00(02(22(20(00(02(21(10(00(02(22(21(12(22(20(01(11(10(01(12(21(11(11(11(x1)))))))))))))))))))))))))))))) → 22(21(11(12(21(10(01(10(00(02(20(00(02(20(02(21(12(20(02(22(22(22(20(00(02(21(11(12(21(11(x1)))))))))))))))))))))))))))))) (439)
22(22(20(02(22(20(00(02(22(20(00(02(21(10(00(02(22(21(12(22(20(01(11(10(01(12(21(11(11(10(x1)))))))))))))))))))))))))))))) → 22(21(11(12(21(10(01(10(00(02(20(00(02(20(02(21(12(20(02(22(22(22(20(00(02(21(11(12(21(10(x1)))))))))))))))))))))))))))))) (440)
22(22(20(02(22(20(00(02(22(20(00(02(21(10(00(02(22(21(12(22(20(01(11(10(01(12(21(11(11(12(x1)))))))))))))))))))))))))))))) → 22(21(11(12(21(10(01(10(00(02(20(00(02(20(02(21(12(20(02(22(22(22(20(00(02(21(11(12(21(12(x1)))))))))))))))))))))))))))))) (441)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[22(x1)] = 1 · x1
[20(x1)] = 1 · x1
[01(x1)] = 1 · x1
[12(x1)] = 1 · x1
[00(x1)] = 1 · x1
[10(x1)] = 1 · x1
[21(x1)] = 1 · x1 + 1
[11(x1)] = 1 · x1 + 4
[02(x1)] = 1 · x1
all of the following rules can be deleted.
22(20(01(12(22(20(00(01(10(01(12(21(11(10(02(20(01(12(21(10(02(20(01(12(22(22(21(12(21(11(x1)))))))))))))))))))))))))))))) → 21(10(02(21(10(02(21(12(22(22(20(00(02(20(00(01(10(01(12(21(12(22(21(10(01(12(21(12(21(11(x1)))))))))))))))))))))))))))))) (451)
22(20(01(12(22(20(00(01(10(01(12(21(11(10(02(20(01(12(21(10(02(20(01(12(22(22(21(12(21(10(x1)))))))))))))))))))))))))))))) → 21(10(02(21(10(02(21(12(22(22(20(00(02(20(00(01(10(01(12(21(12(22(21(10(01(12(21(12(21(10(x1)))))))))))))))))))))))))))))) (452)
22(20(01(12(22(20(00(01(10(01(12(21(11(10(02(20(01(12(21(10(02(20(01(12(22(22(21(12(21(12(x1)))))))))))))))))))))))))))))) → 21(10(02(21(10(02(21(12(22(22(20(00(02(20(00(01(10(01(12(21(12(22(21(10(01(12(21(12(21(12(x1)))))))))))))))))))))))))))))) (453)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[11(x1)] = 1 · x1 + 1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[02(x1)] = 1 · x1
[00(x1)] = 1 · x1
[01(x1)] = 1 · x1
[21(x1)] = 1 · x1
[10(x1)] = 1 · x1
[22(x1)] = 1 · x1
all of the following rules can be deleted.
11(12(20(02(20(00(01(11(12(21(10(01(10(02(22(22(22(22(22(22(22(20(00(01(11(11(11(11(12(21(x1)))))))))))))))))))))))))))))) → 12(21(10(02(21(10(00(01(11(11(12(21(10(01(10(00(01(11(12(21(10(02(22(22(21(11(11(10(02(21(x1)))))))))))))))))))))))))))))) (487)
11(12(20(02(20(00(01(11(12(21(10(01(10(02(22(22(22(22(22(22(22(20(00(01(11(11(11(11(12(20(x1)))))))))))))))))))))))))))))) → 12(21(10(02(21(10(00(01(11(11(12(21(10(01(10(00(01(11(12(21(10(02(22(22(21(11(11(10(02(20(x1)))))))))))))))))))))))))))))) (488)
11(12(20(02(20(00(01(11(12(21(10(01(10(02(22(22(22(22(22(22(22(20(00(01(11(11(11(11(12(22(x1)))))))))))))))))))))))))))))) → 12(21(10(02(21(10(00(01(11(11(12(21(10(01(10(00(01(11(12(21(10(02(22(22(21(11(11(10(02(22(x1)))))))))))))))))))))))))))))) (489)

1.1.1.1.1.1.1.1.1.1 R is empty

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