Input TRS:
    1: a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
    2: a(a(x)) -> f(b(),a(f(a(x),b())))
    3: f(a(x),b()) -> f(b(),a(x))
Number of Rules: 3
Direct QWPOS(mPol) ... failed.