MAYBE
Time: 0.008116
TRS:
 {            p 0() -> 0(),
              p s x -> x,
      minus(x, 0()) -> x,
      minus(x, s y) -> p minus(x, y),
    minus(s x, s y) -> minus(x, y),
      div(0(), s y) -> 0(),
      div(s x, s y) -> s div(minus(s x, s y), s y),
  log(s 0(), s s y) -> 0(),
  log(s s x, s s y) -> s log(div(minus(x, y), s s y), s s y)}
 DP:
  DP:
   {    minus#(x, s y) -> p# minus(x, y),
        minus#(x, s y) -> minus#(x, y),
      minus#(s x, s y) -> minus#(x, y),
        div#(s x, s y) -> minus#(s x, s y),
        div#(s x, s y) -> div#(minus(s x, s y), s y),
    log#(s s x, s s y) -> minus#(x, y),
    log#(s s x, s s y) -> div#(minus(x, y), s s y),
    log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y)}
  TRS:
  {            p 0() -> 0(),
               p s x -> x,
       minus(x, 0()) -> x,
       minus(x, s y) -> p minus(x, y),
     minus(s x, s y) -> minus(x, y),
       div(0(), s y) -> 0(),
       div(s x, s y) -> s div(minus(s x, s y), s y),
   log(s 0(), s s y) -> 0(),
   log(s s x, s s y) -> s log(div(minus(x, y), s s y), s s y)}
  UR:
   {          p 0() -> 0(),
              p s x -> x,
      minus(x, 0()) -> x,
      minus(x, s y) -> p minus(x, y),
    minus(s x, s y) -> minus(x, y),
      div(0(), s y) -> 0(),
      div(s x, s y) -> s div(minus(s x, s y), s y),
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y))
     (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> div#(minus(x, y), s s y))
     (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> minus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
     (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> div#(minus(s x, s y), s y))
     (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> minus#(s x, s y))
     (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> p# minus(x, y))
     (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> minus#(x, y))
     (div#(s x, s y) -> minus#(s x, s y), minus#(s x, s y) -> minus#(x, y))
     (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
     (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
     (log#(s s x, s s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> minus#(s x, s y))
     (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> div#(minus(s x, s y), s y))}
    EDG:
     {(log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y))
      (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> div#(minus(x, y), s s y))
      (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> minus#(x, y))
      (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
      (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
      (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> div#(minus(s x, s y), s y))
      (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> minus#(s x, s y))
      (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> p# minus(x, y))
      (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> minus#(x, y))
      (div#(s x, s y) -> minus#(s x, s y), minus#(s x, s y) -> minus#(x, y))
      (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
      (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
      (log#(s s x, s s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
      (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
      (minus#(x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> minus#(s x, s y))
      (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> div#(minus(s x, s y), s y))}
     EDG:
      {(log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y))
       (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> div#(minus(x, y), s s y))
       (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> minus#(x, y))
       (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
       (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
       (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> div#(minus(s x, s y), s y))
       (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> minus#(s x, s y))
       (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> p# minus(x, y))
       (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> minus#(x, y))
       (div#(s x, s y) -> minus#(s x, s y), minus#(s x, s y) -> minus#(x, y))
       (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
       (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
       (log#(s s x, s s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
       (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
       (minus#(x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> minus#(s x, s y))
       (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> div#(minus(s x, s y), s y))}
      EDG:
       {(log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y))
        (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> div#(minus(x, y), s s y))
        (log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y), log#(s s x, s s y) -> minus#(x, y))
        (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
        (minus#(s x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
        (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> div#(minus(s x, s y), s y))
        (div#(s x, s y) -> div#(minus(s x, s y), s y), div#(s x, s y) -> minus#(s x, s y))
        (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> p# minus(x, y))
        (div#(s x, s y) -> minus#(s x, s y), minus#(x, s y) -> minus#(x, y))
        (div#(s x, s y) -> minus#(s x, s y), minus#(s x, s y) -> minus#(x, y))
        (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
        (log#(s s x, s s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
        (log#(s s x, s s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
        (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
        (minus#(x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> minus#(s x, s y))
        (log#(s s x, s s y) -> div#(minus(x, y), s s y), div#(s x, s y) -> div#(minus(s x, s y), s y))}
       STATUS:
        arrows: 0.703125
        SCCS (3):
         Scc:
          {log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y)}
         Scc:
          {div#(s x, s y) -> div#(minus(s x, s y), s y)}
         Scc:
          {  minus#(x, s y) -> minus#(x, y),
           minus#(s x, s y) -> minus#(x, y)}
         
         SCC (1):
          Strict:
           {log#(s s x, s s y) -> log#(div(minus(x, y), s s y), s s y)}
          Weak:
          {            p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
             minus(s x, s y) -> minus(x, y),
               div(0(), s y) -> 0(),
               div(s x, s y) -> s div(minus(s x, s y), s y),
           log(s 0(), s s y) -> 0(),
           log(s s x, s s y) -> s log(div(minus(x, y), s s y), s s y)}
          Open
         
         
         SCC (1):
          Strict:
           {div#(s x, s y) -> div#(minus(s x, s y), s y)}
          Weak:
          {            p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
             minus(s x, s y) -> minus(x, y),
               div(0(), s y) -> 0(),
               div(s x, s y) -> s div(minus(s x, s y), s y),
           log(s 0(), s s y) -> 0(),
           log(s s x, s s y) -> s log(div(minus(x, y), s s y), s s y)}
          Open
         
         SCC (2):
          Strict:
           {  minus#(x, s y) -> minus#(x, y),
            minus#(s x, s y) -> minus#(x, y)}
          Weak:
          {            p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
             minus(s x, s y) -> minus(x, y),
               div(0(), s y) -> 0(),
               div(s x, s y) -> s div(minus(s x, s y), s y),
           log(s 0(), s s y) -> 0(),
           log(s s x, s s y) -> s log(div(minus(x, y), s s y), s s y)}
          Open