Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/baabababba-abababbaababab.srs)

The rewrite relation of the following TRS is considered.

b(a(a(b(a(b(a(b(b(a(x1)))))))))) → a(b(a(b(a(b(b(a(a(b(a(b(a(b(x1)))))))))))))) (1)

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
a(b(b(a(b(a(b(a(a(b(x1)))))))))) → b(a(b(a(b(a(a(b(b(a(b(a(b(a(x1)))))))))))))) (2)

1.1 Closure Under Flat Contexts

Using the flat contexts

{a(☐), b(☐)}

We obtain the transformed TRS
a(a(b(b(a(b(a(b(a(a(b(x1))))))))))) → a(b(a(b(a(b(a(a(b(b(a(b(a(b(a(x1))))))))))))))) (3)
b(a(b(b(a(b(a(b(a(a(b(x1))))))))))) → b(b(a(b(a(b(a(a(b(b(a(b(a(b(a(x1))))))))))))))) (4)

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ab(ba(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1))))))))))))))) (5)
aa(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ab(ba(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1))))))))))))))) (6)
ba(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → bb(ba(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1))))))))))))))) (7)
ba(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → bb(ba(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1))))))))))))))) (8)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1)))))))))))))) (9)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1)))))))))))) (10)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1)))))))))) (11)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → aa#(ab(bb(ba(ab(ba(ab(ba(aa(x1))))))))) (12)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(ab(ba(aa(x1)))))) (13)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(aa(x1)))) (14)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(aa(x1)) (15)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → aa#(x1) (16)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1)))))))))))))) (17)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1)))))))))))) (18)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1)))))))))) (19)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → aa#(ab(bb(ba(ab(ba(ab(ba(ab(x1))))))))) (20)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(ab(ba(ab(x1)))))) (21)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(ab(x1)))) (22)
aa#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(x1)) (23)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1)))))))))))))) (24)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1)))))))))))) (25)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(aa(ab(bb(ba(ab(ba(ab(ba(aa(x1)))))))))) (26)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → aa#(ab(bb(ba(ab(ba(ab(ba(aa(x1))))))))) (27)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(ab(ba(aa(x1)))))) (28)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(ab(ba(aa(x1)))) (29)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → ba#(aa(x1)) (30)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(ba(x1))))))))))) → aa#(x1) (31)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1)))))))))))))) (32)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1)))))))))))) (33)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(aa(ab(bb(ba(ab(ba(ab(ba(ab(x1)))))))))) (34)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → aa#(ab(bb(ba(ab(ba(ab(ba(ab(x1))))))))) (35)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(ab(ba(ab(x1)))))) (36)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(ba(ab(x1)))) (37)
ba#(ab(bb(ba(ab(ba(ab(ba(aa(ab(bb(x1))))))))))) → ba#(ab(x1)) (38)

1.1.1.1.1 Semantic Labeling Processor

The following interpretations form a model of the rules.

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

[bb(x1)] = 1
[ba(x1)] = 1x1
[aa#(x1)] = 0
[ba#(x1)] = 0
[ab(x1)] = 1x1
[aa(x1)] = 0

We obtain the set of labeled pairs
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1)))))))))))))) (39)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1)))))))))))))) (40)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1)))))))))))))) (41)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1)))))))))))))) (42)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1)))))))))))) (43)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1)))))))))))) (44)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1)))))))))) (45)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1)))))))))) (46)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1))))))))) (47)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1))))))))) (48)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa0(x1)))))) (49)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(x1)))))) (50)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(aa0(x1)))) (51)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(aa1(x1)))) (52)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(aa0(x1)) (53)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(aa1(x1)) (54)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → aa#0(x1) (55)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → aa#1(x1) (56)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1)))))))))))))) (57)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1)))))))))))))) (58)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1)))))))))))) (59)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1)))))))))))) (60)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1)))))))))) (61)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1)))))))))) (62)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1))))))))) (63)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → aa#1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1))))))))) (64)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(ab0(x1)))))) (65)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#1(ab1(ba1(ab1(ba1(ab1(x1)))))) (66)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(ab0(x1)))) (67)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#1(ab1(ba1(ab1(x1)))) (68)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(x1)) (69)
ba#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#1(ab1(x1)) (70)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1)))))))))))) (71)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1)))))))))))) (72)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1)))))))))) (73)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1)))))))))) (74)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1))))))))) (75)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1))))))))) (76)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa0(x1)))))) (77)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(x1)))))) (78)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(ab0(ba0(aa0(x1)))) (79)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(ab0(ba0(aa1(x1)))) (80)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ba#0(aa0(x1)) (81)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ba#0(aa1(x1)) (82)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → aa#0(x1) (83)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → aa#1(x1) (84)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1)))))))))))))) (85)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1)))))))))))))) (86)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1)))))))))))) (87)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#0(ab0(ba0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1)))))))))))) (88)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1)))))))))) (89)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1)))))))))) (90)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1))))))))) (91)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → aa#1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1))))))))) (92)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(ab0(ba0(ab0(x1)))))) (93)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#1(ab1(ba1(ab1(ba1(ab1(x1)))))) (94)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(ba0(ab0(x1)))) (95)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#1(ab1(ba1(ab1(x1)))) (96)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ba#0(ab0(x1)) (97)
aa#1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ba#1(ab1(x1)) (98)
and the set of labeled rules:
aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → ab0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1))))))))))))))) (99)
aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → ab0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1))))))))))))))) (100)
aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → ab0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1))))))))))))))) (101)
aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → ab0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1))))))))))))))) (102)
ba1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(ab0(ba0(x1))))))))))) → bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa0(x1))))))))))))))) (103)
ba1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(ba1(x1))))))))))) → bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(x1))))))))))))))) (104)
ba1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(x1))))))))))) → bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(ab0(x1))))))))))))))) (105)
ba1(ab1(bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(x1))))))))))) → bb0(ba0(ab0(ba0(ab0(ba0(aa1(ab1(bb1(ba1(ab1(ba1(ab1(ba1(ab1(x1))))))))))))))) (106)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.