Certification Problem

Input (TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-362)

The rewrite relation of the following TRS is considered.

a(x1)	→	b(x1)	(1)
a(b(b(c(x1))))	→	b(c(c(a(a(a(x1))))))	(2)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

a b b c b b c c b c c →⁺ b c c b c c b c c a b c c a b b c b b c c b c c a a a

The derivation can be derived as follows.

a b b c →⁺ b c c a a a: This is an original rule (OC1).
a →⁺ b: This is an original rule (OC1).
a b b c →⁺ b c c a b a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c →⁺ b c c a a a
- a →⁺ b
a b b c →⁺ b c c a a b: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c →⁺ b c c a a a
- a →⁺ b
a b b c →⁺ b c c a b b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c →⁺ b c c a a b
- a →⁺ b
a b b c b b c →⁺ b c c a b b c c a b b: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c →⁺ b c c a b a
- a b b c →⁺ b c c a b b
a b b c b b c →⁺ b c c b c c a a a c a b b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c →⁺ b c c a b b c c a b b
- a b b c →⁺ b c c a a a
a b b c b b c →⁺ b c c b c c a b a c a b b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c →⁺ b c c b c c a a a c a b b
- a →⁺ b
a b b c b b c →⁺ b c c b c c a b b c a b b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c →⁺ b c c b c c a b a c a b b
- a →⁺ b
a b b c b b c c →⁺ b c c b c c a b b c b c c a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c b b c →⁺ b c c b c c a b b c a b b
- a b b c →⁺ b c c a a a
a b b c b b c c →⁺ b c c b c c a b b c b c c a a b: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c b b c c →⁺ b c c b c c a b b c b c c a a a
- a →⁺ b
a b b c b b c c →⁺ b c c b c c a b b c b c c b a b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c →⁺ b c c b c c a b b c b c c a a b
- a →⁺ b
a b b c b b c c →⁺ b c c b c c b c c a a a b c c b a b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c →⁺ b c c b c c a b b c b c c b a b
- a b b c →⁺ b c c a a a
a b b c b b c c →⁺ b c c b c c b c c a a b b c c b a b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c →⁺ b c c b c c b c c a a a b c c b a b
- a →⁺ b
a b b c b b c c →⁺ b c c b c c b c c a b c c a a a c b a b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c →⁺ b c c b c c b c c a a b b c c b a b
- a b b c →⁺ b c c a a a
a b b c b b c c →⁺ b c c b c c b c c a b c c a b a c b a b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c →⁺ b c c b c c b c c a b c c a a a c b a b
- a →⁺ b
a b b c b b c c →⁺ b c c b c c b c c a b c c a b b c b a b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c →⁺ b c c b c c b c c a b c c a b a c b a b
- a →⁺ b
a b b c b b c c b c →⁺ b c c b c c b c c a b c c a b b c b b c c a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c b b c c →⁺ b c c b c c b c c a b c c a b b c b a b
- a b b c →⁺ b c c a a a
a b b c b b c c b c →⁺ b c c b c c b c c a b c c a b b c b b c c a a b: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c b b c c b c →⁺ b c c b c c b c c a b c c a b b c b b c c a a a
- a →⁺ b
a b b c b b c c b c →⁺ b c c b c c b c c a b c c a b b c b b c c a b b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b b c b b c c b c →⁺ b c c b c c b c c a b c c a b b c b b c c a a b
- a →⁺ b
a b b c b b c c b c c →⁺ b c c b c c b c c a b c c a b b c b b c c b c c a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b b c b b c c b c →⁺ b c c b c c b c c a b c c a b b c b b c c a b b
- a b b c →⁺ b c c a a a