MAYBE
Time: 0.002503
TRS:
 {           le(s x, s y) -> le(x, y),
             le(s x, 0()) -> false(),
               le(0(), y) -> true(),
             plus(s x, y) -> s plus(x, y),
             plus(0(), y) -> y,
            times(s x, y) -> plus(y, times(x, y)),
            times(0(), y) -> 0(),
            log(x, s 0()) -> baseError(),
              log(x, 0()) -> baseError(),
          log(s x, s s b) -> loop(s x, s s b, s 0(), 0()),
          log(0(), s s b) -> logZeroError(),
   loop(x, s s b, s y, z) -> if(le(x, s y), x, s s b, s y, z),
  if(false(), x, b, y, z) -> loop(x, b, times(b, y), s z),
   if(true(), x, b, y, z) -> z}
 DP:
  DP:
   {           le#(s x, s y) -> le#(x, y),
               plus#(s x, y) -> plus#(x, y),
              times#(s x, y) -> plus#(y, times(x, y)),
              times#(s x, y) -> times#(x, y),
            log#(s x, s s b) -> loop#(s x, s s b, s 0(), 0()),
     loop#(x, s s b, s y, z) -> le#(x, s y),
     loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z),
    if#(false(), x, b, y, z) -> times#(b, y),
    if#(false(), x, b, y, z) -> loop#(x, b, times(b, y), s z)}
  TRS:
  {           le(s x, s y) -> le(x, y),
              le(s x, 0()) -> false(),
                le(0(), y) -> true(),
              plus(s x, y) -> s plus(x, y),
              plus(0(), y) -> y,
             times(s x, y) -> plus(y, times(x, y)),
             times(0(), y) -> 0(),
             log(x, s 0()) -> baseError(),
               log(x, 0()) -> baseError(),
           log(s x, s s b) -> loop(s x, s s b, s 0(), 0()),
           log(0(), s s b) -> logZeroError(),
    loop(x, s s b, s y, z) -> if(le(x, s y), x, s s b, s y, z),
   if(false(), x, b, y, z) -> loop(x, b, times(b, y), s z),
    if(true(), x, b, y, z) -> z}
  UR:
   { le(s x, s y) -> le(x, y),
     le(s x, 0()) -> false(),
       le(0(), y) -> true(),
     plus(s x, y) -> s plus(x, y),
     plus(0(), y) -> y,
    times(s x, y) -> plus(y, times(x, y)),
    times(0(), y) -> 0(),
          a(w, v) -> w,
          a(w, v) -> v}
   EDG:
    {(if#(false(), x, b, y, z) -> loop#(x, b, times(b, y), s z), loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z))
     (if#(false(), x, b, y, z) -> loop#(x, b, times(b, y), s z), loop#(x, s s b, s y, z) -> le#(x, s y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (if#(false(), x, b, y, z) -> times#(b, y), times#(s x, y) -> times#(x, y))
     (if#(false(), x, b, y, z) -> times#(b, y), times#(s x, y) -> plus#(y, times(x, y)))
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
     (loop#(x, s s b, s y, z) -> le#(x, s y), le#(s x, s y) -> le#(x, y))
     (loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z), if#(false(), x, b, y, z) -> times#(b, y))
     (loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z), if#(false(), x, b, y, z) -> loop#(x, b, times(b, y), s z))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (log#(s x, s s b) -> loop#(s x, s s b, s 0(), 0()), loop#(x, s s b, s y, z) -> le#(x, s y))
     (log#(s x, s s b) -> loop#(s x, s s b, s 0(), 0()), loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z))}
    STATUS:
     arrows: 0.827160
     SCCS (4):
      Scc:
       { loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z),
        if#(false(), x, b, y, z) -> loop#(x, b, times(b, y), s z)}
      Scc:
       {times#(s x, y) -> times#(x, y)}
      Scc:
       {plus#(s x, y) -> plus#(x, y)}
      Scc:
       {le#(s x, s y) -> le#(x, y)}
      
      
      SCC (2):
       Strict:
        { loop#(x, s s b, s y, z) -> if#(le(x, s y), x, s s b, s y, z),
         if#(false(), x, b, y, z) -> loop#(x, b, times(b, y), s z)}
       Weak:
       {           le(s x, s y) -> le(x, y),
                   le(s x, 0()) -> false(),
                     le(0(), y) -> true(),
                   plus(s x, y) -> s plus(x, y),
                   plus(0(), y) -> y,
                  times(s x, y) -> plus(y, times(x, y)),
                  times(0(), y) -> 0(),
                  log(x, s 0()) -> baseError(),
                    log(x, 0()) -> baseError(),
                log(s x, s s b) -> loop(s x, s s b, s 0(), 0()),
                log(0(), s s b) -> logZeroError(),
         loop(x, s s b, s y, z) -> if(le(x, s y), x, s s b, s y, z),
        if(false(), x, b, y, z) -> loop(x, b, times(b, y), s z),
         if(true(), x, b, y, z) -> z}
       Open
      
      SCC (1):
       Strict:
        {times#(s x, y) -> times#(x, y)}
       Weak:
       {           le(s x, s y) -> le(x, y),
                   le(s x, 0()) -> false(),
                     le(0(), y) -> true(),
                   plus(s x, y) -> s plus(x, y),
                   plus(0(), y) -> y,
                  times(s x, y) -> plus(y, times(x, y)),
                  times(0(), y) -> 0(),
                  log(x, s 0()) -> baseError(),
                    log(x, 0()) -> baseError(),
                log(s x, s s b) -> loop(s x, s s b, s 0(), 0()),
                log(0(), s s b) -> logZeroError(),
         loop(x, s s b, s y, z) -> if(le(x, s y), x, s s b, s y, z),
        if(false(), x, b, y, z) -> loop(x, b, times(b, y), s z),
         if(true(), x, b, y, z) -> z}
       Open
      
      SCC (1):
       Strict:
        {plus#(s x, y) -> plus#(x, y)}
       Weak:
       {           le(s x, s y) -> le(x, y),
                   le(s x, 0()) -> false(),
                     le(0(), y) -> true(),
                   plus(s x, y) -> s plus(x, y),
                   plus(0(), y) -> y,
                  times(s x, y) -> plus(y, times(x, y)),
                  times(0(), y) -> 0(),
                  log(x, s 0()) -> baseError(),
                    log(x, 0()) -> baseError(),
                log(s x, s s b) -> loop(s x, s s b, s 0(), 0()),
                log(0(), s s b) -> logZeroError(),
         loop(x, s s b, s y, z) -> if(le(x, s y), x, s s b, s y, z),
        if(false(), x, b, y, z) -> loop(x, b, times(b, y), s z),
         if(true(), x, b, y, z) -> z}
       Open
      
      SCC (1):
       Strict:
        {le#(s x, s y) -> le#(x, y)}
       Weak:
       {           le(s x, s y) -> le(x, y),
                   le(s x, 0()) -> false(),
                     le(0(), y) -> true(),
                   plus(s x, y) -> s plus(x, y),
                   plus(0(), y) -> y,
                  times(s x, y) -> plus(y, times(x, y)),
                  times(0(), y) -> 0(),
                  log(x, s 0()) -> baseError(),
                    log(x, 0()) -> baseError(),
                log(s x, s s b) -> loop(s x, s s b, s 0(), 0()),
                log(0(), s s b) -> logZeroError(),
         loop(x, s s b, s y, z) -> if(le(x, s y), x, s s b, s y, z),
        if(false(), x, b, y, z) -> loop(x, b, times(b, y), s z),
         if(true(), x, b, y, z) -> z}
       Open