YES
(VAR X Y Z I P X1 X2)
(RULES 
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)
)

Proving termination of rewriting for PALINDROME_nosorts_GM:

-> Dependency pairs:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_a____(__(X,Y),Z) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_a____(__(X,Y),Z) -> nF_mark(Y)
nF_a____(__(X,Y),Z) -> nF_mark(Z)
nF_a____(X,nil) -> nF_mark(X)
nF_a____(nil,X) -> nF_mark(X)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_mark(__(X1,X2)) -> nF_mark(X2)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(isNePal(X)) -> nF_a__isNePal(mark(X))
nF_mark(isNePal(X)) -> nF_mark(X)

-> Proof of termination for PALINDROME_nosorts_GM_1:
-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_mark(isNePal(X)) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(__(X1,X2)) -> nF_mark(X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_a____(nil,X) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_a____(X,nil) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_mark(Z)
nF_a____(__(X,Y),Z) -> nF_mark(Y)
nF_a____(__(X,Y),Z) -> nF_mark(X)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X1 + X2
[tt] = 0
[a__isNePal](X) = X
[and](X1,X2) = X1 + X2
[isNePal](X) = X
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.7407e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a____(__(X,Y),Z) -> nF_mark(Y)
nF_a____(__(X,Y),Z) -> nF_mark(Z)
nF_a____(X,nil) -> nF_mark(X)
nF_a____(nil,X) -> nF_mark(X)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_mark(__(X1,X2)) -> nF_mark(X2)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(isNePal(X)) -> nF_mark(X)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X1 + X2
[tt] = 1
[a__isNePal](X) = X + 1
[and](X1,X2) = X1 + X2
[isNePal](X) = X + 1
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.7433e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(__(X1,X2)) -> nF_mark(X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_a____(nil,X) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_a____(X,nil) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_mark(Z)
nF_a____(__(X,Y),Z) -> nF_mark(Y)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X1 + X2
[tt] = 0
[a__isNePal](X) = 0
[and](X1,X2) = X1 + X2
[isNePal](X) = 0
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.4036e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a____(__(X,Y),Z) -> nF_mark(Z)
nF_a____(X,nil) -> nF_mark(X)
nF_a____(nil,X) -> nF_mark(X)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_mark(__(X1,X2)) -> nF_mark(X2)
nF_mark(and(X1,X2)) -> nF_mark(X1)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X1 + X2 + 1
[tt] = 1
[a__isNePal](X) = X
[and](X1,X2) = X1 + X2 + 1
[isNePal](X) = X
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.2611e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_mark(__(X1,X2)) -> nF_mark(X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_a____(nil,X) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_a____(X,nil) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_mark(Z)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X2
[tt] = 1
[a__isNePal](X) = 1
[and](X1,X2) = X2
[isNePal](X) = 1
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.3561e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a____(X,nil) -> nF_mark(X)
nF_a____(nil,X) -> nF_mark(X)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_mark(__(X1,X2)) -> nF_mark(X2)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X2
[tt] = 1
[a__isNePal](X) = X
[and](X1,X2) = X2
[isNePal](X) = X
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.6337e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_mark(__(X1,X2)) -> nF_mark(X1)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_a____(nil,X) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_a____(X,nil) -> nF_mark(X)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2
[__](X1,X2) = X1 + X2
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X2
[tt] = 0
[a__isNePal](X) = 0
[and](X1,X2) = X2
[isNePal](X) = 0
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.2326e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a____(nil,X) -> nF_mark(X)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_mark(__(X1,X2)) -> nF_mark(X1)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X2
[tt] = 1
[a__isNePal](X) = X
[and](X1,X2) = X2
[isNePal](X) = X
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.143399999999998e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)
nF_a____(nil,X) -> nF_mark(X)
nF_a____(__(X,Y),Z) -> nF_a____(mark(Y),mark(Z))

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X2
[tt] = 1
[a__isNePal](X) = X
[and](X1,X2) = X2
[isNePal](X) = X
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.2358e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a____(nil,X) -> nF_mark(X)
nF_a__and(tt,X) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2
[__](X1,X2) = X1 + X2
[mark](X) = X
[nil] = 0
[a__and](X1,X2) = X2 + 1
[tt] = 1
[a__isNePal](X) = 1
[and](X1,X2) = X2 + 1
[isNePal](X) = 1
[nF_a____](X1,X2) = X1 + X2
[nF_mark](X) = X
[nF_a__and](X1,X2) = X2

TIME: 5.1428e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))
nF_mark(__(X1,X2)) -> nF_a____(mark(X1),mark(X2))
nF_a____(nil,X) -> nF_mark(X)

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 0
[a__and](X1,X2) = X2
[tt] = 0
[a__isNePal](X) = 0
[and](X1,X2) = X2
[isNePal](X) = 0
[nF_a____](X1,X2) = X1 + X2 + 1
[nF_mark](X) = X

TIME: 5.0513e-2

-> -> Dependency pairs in cycle:
nF_a____(__(X,Y),Z) -> nF_a____(mark(X),a____(mark(Y),mark(Z)))

UsableRules:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil) -> mark(X)
a____(nil,X) -> mark(X)
a__and(tt,X) -> mark(X)
a__isNePal(__(I,__(P,I))) -> tt
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil) -> nil
mark(tt) -> tt
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(X)

Polynomial Interpretation:

[a____](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[mark](X) = X
[nil] = 1
[a__and](X1,X2) = X2
[tt] = 1
[a__isNePal](X) = X
[and](X1,X2) = X2
[isNePal](X) = X
[nF_a____](X1,X2) = X1

TIME: 4.959e-2


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



Termination was proved succesfully.