(1) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
a b c b c c → c c c c c c c c c a b c b c c c
a b c b c c →
c c c c c c c c c a b c b c c cby OverlapClosure OC 2
a b c b c → c c c c c c c c c a b c b b
by OverlapClosure OC 3a b c b c → c c c c c c a b c c b b
by OverlapClosure OC 3a b c b c → c c c a b c c c b b
by OverlapClosure OC 2a → b
by original rule (OC 1)
b b c b c → c c c a b c c c b b
by OverlapClosure OC 2b b c → c c c a a
by OverlapClosure OC 3b b c → a c c c a a
by original rule (OC 1)
a →
by original rule (OC 1)
a b c → b c c c b b
by OverlapClosure OC 2a → b
by original rule (OC 1)
b b c → b c c c b b
by OverlapClosure OC 3b b c → b c c c a b
by OverlapClosure OC 3b b c → a c c c a b
by OverlapClosure OC 2b b c → a c c c a a
by original rule (OC 1)
a → b
by original rule (OC 1)
a → b
by original rule (OC 1)
a → b
by original rule (OC 1)
a b c → c c c a b
by OverlapClosure OC 2a → b
by original rule (OC 1)
b b c → c c c a b
by OverlapClosure OC 2b b c → c c c a a
by OverlapClosure OC 3b b c → a c c c a a
by original rule (OC 1)
a →
by original rule (OC 1)
a → b
by original rule (OC 1)
a b c → c c c a b
by OverlapClosure OC 2a → b
by original rule (OC 1)
b b c → c c c a b
by OverlapClosure OC 2b b c → c c c a a
by OverlapClosure OC 3b b c → a c c c a a
by original rule (OC 1)
a →
by original rule (OC 1)
a → b
by original rule (OC 1)
b b c → b c c c
by OverlapClosure OC 2b b c → b c c c a
by OverlapClosure OC 3b b c → a c c c a
by OverlapClosure OC 2b b c → a c c c a a
by original rule (OC 1)
a →
by original rule (OC 1)
a → b
by original rule (OC 1)
a →
by original rule (OC 1)