Input TRS:
    1: a__f(f(a())) -> a__f(g(f(a())))
    2: mark(f(X)) -> a__f(mark(X))
    3: mark(a()) -> a()
    4: mark(g(X)) -> g(X)
    5: a__f(X) -> f(X)
Number of Rules: 5
Direct QWPOS(max) ... failed.