YES
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())) --> false()
Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ... succeeded.
     s(x1)	weight: x1	status: x1
   ack(x1,x2)	weight: x2	status: x2
 seven()	weight: (/ 1 4)	status: []	precedence above: s O
 false()	weight: (/ 7 8)	status: []	precedence above:
     O()	weight: (/ 1 8)	status: []	precedence above: s
  true()	weight: (/ 1 2)	status: []	precedence above:
    #(x1)	weight: x1	status: []	precedence above:
 isNat(x1)	weight: (/ 1 2) + x1	status: []	precedence above: false