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(U11(tt())) -> mark(U12(tt()))
    5: active(U12(tt())) -> mark(tt())
    6: active(isNePal(zz(I,zz(P,I)))) -> mark(U11(tt()))
    7: active(zz(X1,X2)) -> zz(active(X1),X2)
    8: active(zz(X1,X2)) -> zz(X1,active(X2))
    9: active(U11(X)) -> U11(active(X))
    10: active(U12(X)) -> U12(active(X))
    11: active(isNePal(X)) -> isNePal(active(X))
    12: zz(mark(X1),X2) -> mark(zz(X1,X2))
    13: zz(X1,mark(X2)) -> mark(zz(X1,X2))
    14: U11(mark(X)) -> mark(U11(X))
    15: U12(mark(X)) -> mark(U12(X))
    16: isNePal(mark(X)) -> mark(isNePal(X))
    17: proper(zz(X1,X2)) -> zz(proper(X1),proper(X2))
    18: proper(nil()) -> ok(nil())
    19: proper(U11(X)) -> U11(proper(X))
    20: proper(tt()) -> ok(tt())
    21: proper(U12(X)) -> U12(proper(X))
    22: proper(isNePal(X)) -> isNePal(proper(X))
    23: zz(ok(X1),ok(X2)) -> ok(zz(X1,X2))
    24: U11(ok(X)) -> ok(U11(X))
    25: U12(ok(X)) -> ok(U12(X))
    26: isNePal(ok(X)) -> ok(isNePal(X))
    27: top(mark(X)) -> top(proper(X))
    28: top(ok(X)) -> top(active(X))
Number of Rules: 28
Direct QWPOS(mPol) ... failed.