YES
Time: 0.028759
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:
  DP:
   {             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())}
  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())}
  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) -> le#(s x, y), le#(s x, s y) -> le#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y))
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, y) -> le#(s x, y))
    (if_minus#(false(), s x, y) -> minus#(x, y), minus#(s x, y) -> le#(s x, y))
    (if_minus#(false(), s x, y) -> minus#(x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, 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) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))
    (minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(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 (4):
    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 (1):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if_minus](x0, x1, x2) = x0,
       
       [le](x0, x1) = x0 + 1,
       
       [minus](x0, x1) = x0,
       
       [quot](x0, x1) = x0,
       
       [s](x0) = x0 + 1,
       
       [log](x0) = x0 + 1,
       
       [true] = 0,
       
       [0] = 0,
       
       [false] = 0,
       
       [log#](x0) = x0 + 1
      Strict:
       log# s s x -> log# s quot(x, s s 0())
       3 + 1x >= 2 + 1x
      Weak:
       
     Qed
   SCC (1):
    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:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [if_minus](x0, x1, x2) = x0,
      
      [le](x0, x1) = x0 + 1,
      
      [minus](x0, x1) = x0,
      
      [quot](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [log](x0) = x0,
      
      [true] = 0,
      
      [0] = 1,
      
      [false] = 0,
      
      [quot#](x0, x1) = x0 + 1
     Strict:
      quot#(s x, s y) -> quot#(minus(x, y), s y)
      2 + 0y + 1x >= 1 + 0y + 1x
     Weak:
      
    Qed
   SCC (2):
    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 (0):
       
       Qed
   SCC (1):
    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#) = 1
     Strict:
      {}
     Qed