Input TRS:
    1: active(zz(zz(X,Y),Z)) -> mark(zz(X,zz(Y,Z)))
    2: active(zz(X,nil())) -> mark(X)
    3: active(zz(nil(),X)) -> mark(X)
    4: active(and(tt(),X)) -> mark(X)
    5: active(isNePal(zz(I,zz(P,I)))) -> mark(tt())
    6: active(zz(X1,X2)) -> zz(active(X1),X2)
    7: active(zz(X1,X2)) -> zz(X1,active(X2))
    8: active(and(X1,X2)) -> and(active(X1),X2)
    9: active(isNePal(X)) -> isNePal(active(X))
    10: zz(mark(X1),X2) -> mark(zz(X1,X2))
    11: zz(X1,mark(X2)) -> mark(zz(X1,X2))
    12: and(mark(X1),X2) -> mark(and(X1,X2))
    13: isNePal(mark(X)) -> mark(isNePal(X))
    14: proper(zz(X1,X2)) -> zz(proper(X1),proper(X2))
    15: proper(nil()) -> ok(nil())
    16: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    17: proper(tt()) -> ok(tt())
    18: proper(isNePal(X)) -> isNePal(proper(X))
    19: zz(ok(X1),ok(X2)) -> ok(zz(X1,X2))
    20: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    21: isNePal(ok(X)) -> ok(isNePal(X))
    22: top(mark(X)) -> top(proper(X))
    23: top(ok(X)) -> top(active(X))
Number of Rules: 23
Direct QWPOS(mPol) ... failed.