MAYBE
Input TRS:
    1: ack(s(m),s(n)) -> ack(m,ack(s(m),n))
    2: ack(s(m),O()) -> ack(m,s(O()))
    3: ack(O(),n) -> s(n)
    4: isNat(O()) -> true()
    5: isNat(s(m)) -> isNat(m)
    6: isNat(true()) -> false()
    7: isNat(false()) -> false()
    8: seven() -> s(s(s(s(s(s(s(O())))))))
Infeasibility test:
    isNat(ack(seven(),seven())) --> true()
Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.