YES
Input TRS:
    1: add(0(),x) -> x
    2: add(s(x),y) -> s(add(x,y))
    3: mult(0(),y) -> 0()
    4: mult(s(x),y) -> add(mult(x,y),y)
    5: lte(0(),y) -> true()
    6: lte(s(x),0()) -> false()
    7: lte(s(x),s(y)) -> lte(x,y)
    8: minus(0(),s(y)) -> 0()
    9: minus(x,0()) -> x
    10: minus(s(x),s(y)) -> minus(x,y)
    11: mod(0(),y) -> 0()
    12: mod(x,0()) -> x
    13: mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) --> true()
    14: mod(x,s(y)) -> x | lte(s(y),x) --> false()
    15: div(0(),s(x)) -> 0()
    16: div(s(x),s(y)) -> 0() | lte(s(x),y) --> true()
    17: div(s(x),s(y)) -> s(q) | lte(s(x),y) --> false() | div(minus(x,y),s(y)) --> q
    18: power(x,0()) -> s(0())
    19: power(x,n) -> mult(mult(y,y),s(0())) | n --> s(n') | mod(n,s(s(0()))) --> 0() | power(x,div(n,s(s(0())))) --> y
    20: power(x,n) -> mult(mult(y,y),x) | n --> s(n') | mod(n,s(s(0()))) --> s(z) | power(x,div(n,s(s(0())))) --> y
Infeasibility test:
    lte(s(x2),0()) --> true()
Symbol transition graph:
    mod	-->  # 0 add div false lte minus mod mult power s true
    lte	--> false lte true
    div	--> 0 s
    power	-->  # 0 add div false lte minus mod mult power s true
    add	-->  # 0 add div false lte minus mod mult power s true
    minus	-->  # 0 add div false lte minus mod mult power s true
    mult	-->  # 0 add div false lte minus mod mult power s true
  Collapsable symbols: { add mod mod minus }