Input TRS:
    1: f(x,h(y)) -> h(f(f(h(a()),y),x))
Number of Rules: 1
Direct POLO(mSum) ... failed.