Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nosorts_L)

The rewrite relation of the following TRS is considered.

and(tt) → X (1)
__(__(X,Y),Z) → __(X,__(Y,Z)) (2)
__(X,nil) → X (3)
__(nil,X) → X (4)
isNePal(__(I,__(P,I))) → tt (5)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Variable Condition Violated

The TRS violates one of the two variable conditions. Thus, it is not terminating.