YES
(VAR X Y Z I P X1 X2)
(RULES 
active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
active(__(X,nil)) -> mark(X)
active(__(nil,X)) -> mark(X)
active(U11(tt)) -> mark(U12(tt))
active(U12(tt)) -> mark(tt)
active(isNePal(__(I,__(P,I)))) -> mark(U11(tt))
active(__(X1,X2)) -> __(active(X1),X2)
active(__(X1,X2)) -> __(X1,active(X2))
active(U11(X)) -> U11(active(X))
active(U12(X)) -> U12(active(X))
active(isNePal(X)) -> isNePal(active(X))
__(mark(X1),X2) -> mark(__(X1,X2))
__(X1,mark(X2)) -> mark(__(X1,X2))
U11(mark(X)) -> mark(U11(X))
U12(mark(X)) -> mark(U12(X))
isNePal(mark(X)) -> mark(isNePal(X))
proper(__(X1,X2)) -> __(proper(X1),proper(X2))
proper(nil) -> ok(nil)
proper(U11(X)) -> U11(proper(X))
proper(tt) -> ok(tt)
proper(U12(X)) -> U12(proper(X))
proper(isNePal(X)) -> isNePal(proper(X))
__(ok(X1),ok(X2)) -> ok(__(X1,X2))
U11(ok(X)) -> ok(U11(X))
U12(ok(X)) -> ok(U12(X))
isNePal(ok(X)) -> ok(isNePal(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
)

Proving termination of rewriting for PALINDROME_nosorts_noand_C:

-> Dependency pairs:
nF_active(__(__(X,Y),Z)) -> nF___(X,__(Y,Z))
nF_active(__(__(X,Y),Z)) -> nF___(Y,Z)
nF_active(U11(tt)) -> nF_U12(tt)
nF_active(isNePal(__(I,__(P,I)))) -> nF_U11(tt)
nF_active(__(X1,X2)) -> nF___(active(X1),X2)
nF_active(__(X1,X2)) -> nF_active(X1)
nF_active(__(X1,X2)) -> nF___(X1,active(X2))
nF_active(__(X1,X2)) -> nF_active(X2)
nF_active(U11(X)) -> nF_U11(active(X))
nF_active(U11(X)) -> nF_active(X)
nF_active(U12(X)) -> nF_U12(active(X))
nF_active(U12(X)) -> nF_active(X)
nF_active(isNePal(X)) -> nF_isNePal(active(X))
nF_active(isNePal(X)) -> nF_active(X)
nF___(mark(X1),X2) -> nF___(X1,X2)
nF___(X1,mark(X2)) -> nF___(X1,X2)
nF_U11(mark(X)) -> nF_U11(X)
nF_U12(mark(X)) -> nF_U12(X)
nF_isNePal(mark(X)) -> nF_isNePal(X)
nF_proper(__(X1,X2)) -> nF___(proper(X1),proper(X2))
nF_proper(__(X1,X2)) -> nF_proper(X1)
nF_proper(__(X1,X2)) -> nF_proper(X2)
nF_proper(U11(X)) -> nF_U11(proper(X))
nF_proper(U11(X)) -> nF_proper(X)
nF_proper(U12(X)) -> nF_U12(proper(X))
nF_proper(U12(X)) -> nF_proper(X)
nF_proper(isNePal(X)) -> nF_isNePal(proper(X))
nF_proper(isNePal(X)) -> nF_proper(X)
nF___(ok(X1),ok(X2)) -> nF___(X1,X2)
nF_U11(ok(X)) -> nF_U11(X)
nF_U12(ok(X)) -> nF_U12(X)
nF_isNePal(ok(X)) -> nF_isNePal(X)
nF_top(mark(X)) -> nF_top(proper(X))
nF_top(mark(X)) -> nF_proper(X)
nF_top(ok(X)) -> nF_top(active(X))
nF_top(ok(X)) -> nF_active(X)

-> Proof of termination for PALINDROME_nosorts_noand_C_1_1:
-> -> Dependency pairs in cycle:
nF_top(mark(X)) -> nF_top(proper(X))
nF_top(ok(X)) -> nF_top(active(X))

UsableRules:
active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
active(__(X,nil)) -> mark(X)
active(__(nil,X)) -> mark(X)
active(U11(tt)) -> mark(U12(tt))
active(U12(tt)) -> mark(tt)
active(isNePal(__(I,__(P,I)))) -> mark(U11(tt))
active(__(X1,X2)) -> __(active(X1),X2)
active(__(X1,X2)) -> __(X1,active(X2))
active(U11(X)) -> U11(active(X))
active(U12(X)) -> U12(active(X))
active(isNePal(X)) -> isNePal(active(X))
__(mark(X1),X2) -> mark(__(X1,X2))
__(X1,mark(X2)) -> mark(__(X1,X2))
U11(mark(X)) -> mark(U11(X))
U12(mark(X)) -> mark(U12(X))
isNePal(mark(X)) -> mark(isNePal(X))
proper(__(X1,X2)) -> __(proper(X1),proper(X2))
proper(nil) -> ok(nil)
proper(U11(X)) -> U11(proper(X))
proper(tt) -> ok(tt)
proper(U12(X)) -> U12(proper(X))
proper(isNePal(X)) -> isNePal(proper(X))
__(ok(X1),ok(X2)) -> ok(__(X1,X2))
U11(ok(X)) -> ok(U11(X))
U12(ok(X)) -> ok(U12(X))
isNePal(ok(X)) -> ok(isNePal(X))

Polynomial Interpretation:

[active](X) = X
[__](X1,X2) = 2.X1 + X2 + 1
[mark](X) = X + 1
[nil] = 0
[U11](X) = X + 2
[tt] = 0
[U12](X) = X + 1
[isNePal](X) = X + 1
[proper](X) = X
[ok](X) = X
[top](X) = 0
[nF_top](X) = X

TIME: 5.602e-3

-> -> Dependency pairs in cycle:
nF_top(ok(X)) -> nF_top(active(X))

UsableRules:
active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
active(__(X,nil)) -> mark(X)
active(__(nil,X)) -> mark(X)
active(U11(tt)) -> mark(U12(tt))
active(U12(tt)) -> mark(tt)
active(isNePal(__(I,__(P,I)))) -> mark(U11(tt))
active(__(X1,X2)) -> __(active(X1),X2)
active(__(X1,X2)) -> __(X1,active(X2))
active(U11(X)) -> U11(active(X))
active(U12(X)) -> U12(active(X))
active(isNePal(X)) -> isNePal(active(X))
__(mark(X1),X2) -> mark(__(X1,X2))
__(X1,mark(X2)) -> mark(__(X1,X2))
U11(mark(X)) -> mark(U11(X))
U12(mark(X)) -> mark(U12(X))
isNePal(mark(X)) -> mark(isNePal(X))
__(ok(X1),ok(X2)) -> ok(__(X1,X2))
U11(ok(X)) -> ok(U11(X))
U12(ok(X)) -> ok(U12(X))
isNePal(ok(X)) -> ok(isNePal(X))

Polynomial Interpretation:

[active](X) = X
[__](X1,X2) = X2
[mark](X) = 0
[nil] = 0
[U11](X) = X
[tt] = 0
[U12](X) = X
[isNePal](X) = X
[proper](X) = 0
[ok](X) = X + 1
[top](X) = 0
[nF_top](X) = X

TIME: 1.189e-3


-> Proof of termination for PALINDROME_nosorts_noand_C_1_2:
-> -> Dependency pairs in cycle:
nF_proper(__(X1,X2)) -> nF_proper(X1)
nF_proper(isNePal(X)) -> nF_proper(X)
nF_proper(U12(X)) -> nF_proper(X)
nF_proper(U11(X)) -> nF_proper(X)
nF_proper(__(X1,X2)) -> nF_proper(X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nosorts_noand_C_1_3:
-> -> Dependency pairs in cycle:
nF_active(__(X1,X2)) -> nF_active(X1)
nF_active(isNePal(X)) -> nF_active(X)
nF_active(U12(X)) -> nF_active(X)
nF_active(U11(X)) -> nF_active(X)
nF_active(__(X1,X2)) -> nF_active(X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nosorts_noand_C_1_4:
-> -> Dependency pairs in cycle:
nF_U11(ok(X)) -> nF_U11(X)
nF_U11(mark(X)) -> nF_U11(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nosorts_noand_C_1_5:
-> -> Dependency pairs in cycle:
nF_U12(ok(X)) -> nF_U12(X)
nF_U12(mark(X)) -> nF_U12(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nosorts_noand_C_1_6:
-> -> Dependency pairs in cycle:
nF_isNePal(ok(X)) -> nF_isNePal(X)
nF_isNePal(mark(X)) -> nF_isNePal(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nosorts_noand_C_1_7:
-> -> Dependency pairs in cycle:
nF___(ok(X1),ok(X2)) -> nF___(X1,X2)
nF___(X1,mark(X2)) -> nF___(X1,X2)
nF___(mark(X1),X2) -> nF___(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF___(X1,mark(X2)) -> nF___(X1,X2)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.