Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/97885)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS

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

1.1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS

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

1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

[2(x1)] = 3x1 + 0
[1(x1)] = 3x1 + 1
[0(x1)] = 3x1 + 2

We obtain the labeled TRS

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

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[20(x1)] = x1 +
0
[23(x1)] = x1 +
0
[26(x1)] = x1 +
1
[21(x1)] = x1 +
0
[24(x1)] = x1 +
15825/13
[27(x1)] = x1 +
17625/52
[22(x1)] = x1 +
2377/2
[25(x1)] = x1 +
49277/52
[28(x1)] = x1 +
7/2
[10(x1)] = x1 +
35927/52
[13(x1)] = x1 +
31715/26
[16(x1)] = x1 +
59175/52
[11(x1)] = x1 +
31715/26
[14(x1)] = x1 +
31715/26
[17(x1)] = x1 +
9445/13
[12(x1)] = x1 +
30675/26
[15(x1)] = x1 +
15825/13
[18(x1)] = x1 +
10007/52
[00(x1)] = x1 +
0
[03(x1)] = x1 +
15838/13
[06(x1)] = x1 +
15505/52
[01(x1)] = x1 +
22315/26
[04(x1)] = x1 +
54905/52
[07(x1)] = x1 +
565/26
[02(x1)] = x1 +
5/2
[05(x1)] = x1 +
5/2
[08(x1)] = x1 +
0
all of the following rules can be deleted.

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

1.1.1.1.1 R is empty

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