Certification Problem

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

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

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

The derivation can be derived as follows.

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