Input TRS:
    1: tower(x) -> f(a(),x,s(0()))
    2: f(a(),0(),y) -> y
    3: f(a(),s(x),y) -> f(b(),y,s(x))
    4: f(b(),y,x) -> f(a(),half(x),exp(y))
    5: exp(0()) -> s(0())
    6: exp(s(x)) -> double(exp(x))
    7: double(0()) -> 0()
    8: double(s(x)) -> s(s(double(x)))
    9: half(0()) -> double(0())
    10: half(s(0())) -> half(0())
    11: half(s(s(x))) -> s(half(x))
Number of Rules: 11
Direct QWPOS(Sum) ... failed.