YES
TRS:
 {                le(0(), y) -> true(),
               le(s(x), 0()) -> false(),
              le(s(x), s(y)) -> le(x, y),
               minus(0(), y) -> 0(),
              minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
   if_minus(true(), s(x), y) -> 0(),
  if_minus(false(), s(x), y) -> s(minus(x, y)),
             quot(0(), s(y)) -> 0(),
            quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                 log(s(0())) -> 0(),
                log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
 DP:
  Strict:
   {            le#(s(x), s(y)) -> le#(x, y),
                minus#(s(x), y) -> le#(s(x), y),
                minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y),
    if_minus#(false(), s(x), y) -> minus#(x, y),
              quot#(s(x), s(y)) -> minus#(x, y),
              quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)),
                  log#(s(s(x))) -> quot#(x, s(s(0()))),
                  log#(s(s(x))) -> log#(s(quot(x, s(s(0())))))}
  Weak:
  {                le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
                minus(0(), y) -> 0(),
               minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
    if_minus(true(), s(x), y) -> 0(),
   if_minus(false(), s(x), y) -> s(minus(x, y)),
              quot(0(), s(y)) -> 0(),
             quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                  log(s(0())) -> 0(),
                 log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
  EDG:
   {(log#(s(s(x))) -> log#(s(quot(x, s(s(0()))))), log#(s(s(x))) -> log#(s(quot(x, s(s(0()))))))
    (log#(s(s(x))) -> log#(s(quot(x, s(s(0()))))), log#(s(s(x))) -> quot#(x, s(s(0()))))
    (minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y), if_minus#(false(), s(x), y) -> minus#(x, y))
    (if_minus#(false(), s(x), y) -> minus#(x, y), minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y))
    (if_minus#(false(), s(x), y) -> minus#(x, y), minus#(s(x), y) -> le#(s(x), y))
    (quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)), quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)))
    (quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)), quot#(s(x), s(y)) -> minus#(x, y))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), y) -> le#(s(x), y))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (minus#(s(x), y) -> le#(s(x), y), le#(s(x), s(y)) -> le#(x, y))
    (log#(s(s(x))) -> quot#(x, s(s(0()))), quot#(s(x), s(y)) -> minus#(x, y))
    (log#(s(s(x))) -> quot#(x, s(s(0()))), quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)))}
   SCCS:
    Scc:
     {log#(s(s(x))) -> log#(s(quot(x, s(s(0())))))}
    Scc:
     {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
    Scc:
     {            minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y),
      if_minus#(false(), s(x), y) -> minus#(x, y)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    SCC:
     Strict:
      {log#(s(s(x))) -> log#(s(quot(x, s(s(0())))))}
     Weak:
     {                le(0(), y) -> true(),
                   le(s(x), 0()) -> false(),
                  le(s(x), s(y)) -> le(x, y),
                   minus(0(), y) -> 0(),
                  minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
       if_minus(true(), s(x), y) -> 0(),
      if_minus(false(), s(x), y) -> s(minus(x, y)),
                 quot(0(), s(y)) -> 0(),
                quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                     log(s(0())) -> 0(),
                    log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
     POLY:
      Argument Filtering:
       pi(log#) = 0, pi(log) = [], pi(quot) = 0, pi(if_minus) = 1, pi(minus) = 0, pi(s) = [0], pi(false) = [], pi(0) = [], pi(le) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                le(0(), y) -> true(),
                     le(s(x), 0()) -> false(),
                    le(s(x), s(y)) -> le(x, y),
                     minus(0(), y) -> 0(),
                    minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
         if_minus(true(), s(x), y) -> 0(),
        if_minus(false(), s(x), y) -> s(minus(x, y)),
                   quot(0(), s(y)) -> 0(),
                  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                       log(s(0())) -> 0(),
                      log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
      Qed
    SCC:
     Strict:
      {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
     Weak:
     {                le(0(), y) -> true(),
                   le(s(x), 0()) -> false(),
                  le(s(x), s(y)) -> le(x, y),
                   minus(0(), y) -> 0(),
                  minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
       if_minus(true(), s(x), y) -> 0(),
      if_minus(false(), s(x), y) -> s(minus(x, y)),
                 quot(0(), s(y)) -> 0(),
                quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                     log(s(0())) -> 0(),
                    log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
     POLY:
      Argument Filtering:
       pi(log) = [], pi(quot#) = 0, pi(quot) = [], pi(if_minus) = 1, pi(minus) = 0, pi(s) = [0], pi(false) = [], pi(0) = [], pi(le) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                le(0(), y) -> true(),
                     le(s(x), 0()) -> false(),
                    le(s(x), s(y)) -> le(x, y),
                     minus(0(), y) -> 0(),
                    minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
         if_minus(true(), s(x), y) -> 0(),
        if_minus(false(), s(x), y) -> s(minus(x, y)),
                   quot(0(), s(y)) -> 0(),
                  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                       log(s(0())) -> 0(),
                      log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
      Qed
    SCC:
     Strict:
      {            minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y),
       if_minus#(false(), s(x), y) -> minus#(x, y)}
     Weak:
     {                le(0(), y) -> true(),
                   le(s(x), 0()) -> false(),
                  le(s(x), s(y)) -> le(x, y),
                   minus(0(), y) -> 0(),
                  minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
       if_minus(true(), s(x), y) -> 0(),
      if_minus(false(), s(x), y) -> s(minus(x, y)),
                 quot(0(), s(y)) -> 0(),
                quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                     log(s(0())) -> 0(),
                    log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
     SPSC:
      Simple Projection:
       pi(if_minus#) = 1, pi(minus#) = 0
      Strict:
       {minus#(s(x), y) -> if_minus#(le(s(x), y), s(x), y)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {                le(0(), y) -> true(),
                   le(s(x), 0()) -> false(),
                  le(s(x), s(y)) -> le(x, y),
                   minus(0(), y) -> 0(),
                  minus(s(x), y) -> if_minus(le(s(x), y), s(x), y),
       if_minus(true(), s(x), y) -> 0(),
      if_minus(false(), s(x), y) -> s(minus(x, y)),
                 quot(0(), s(y)) -> 0(),
                quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
                     log(s(0())) -> 0(),
                    log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed