Input TRS:
    1: active(f(x)) -> mark(x)
    2: top(active(c())) -> top(mark(c()))
    3: top(mark(x)) -> top(check(x))
    4: check(f(x)) -> f(check(x))
    5: check(x) -> start(match(f(X()),x))
    6: match(f(x),f(y)) -> f(match(x,y))
    7: match(X(),x) -> proper(x)
    8: proper(c()) -> ok(c())
    9: proper(f(x)) -> f(proper(x))
    10: f(ok(x)) -> ok(f(x))
    11: start(ok(x)) -> found(x)
    12: f(found(x)) -> found(f(x))
    13: top(found(x)) -> top(active(x))
    14: active(f(x)) -> f(active(x))
    15: f(mark(x)) -> mark(f(x))
Number of Rules: 15
Direct QWPOS(Sum) ... failed.