MAYBE
Time: 0.045676
TRS:
 {  minus(X, 0()) -> X,
  minus(s X, s Y) -> p minus(X, Y),
            p s X -> X,
    div(0(), s Y) -> 0(),
    div(s X, s Y) -> s div(minus(X, Y), s Y)}
 DP:
  DP:
   {minus#(s X, s Y) -> minus#(X, Y),
    minus#(s X, s Y) -> p# minus(X, Y),
      div#(s X, s Y) -> minus#(X, Y),
      div#(s X, s Y) -> div#(minus(X, Y), s Y)}
  TRS:
  {  minus(X, 0()) -> X,
   minus(s X, s Y) -> p minus(X, Y),
             p s X -> X,
     div(0(), s Y) -> 0(),
     div(s X, s Y) -> s div(minus(X, Y), s Y)}
  UR:
   {  minus(X, 0()) -> X,
    minus(s X, s Y) -> p minus(X, Y),
              p s X -> X,
            a(x, y) -> x,
            a(x, y) -> y}
   EDG:
    {(minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> p# minus(X, Y))
     (minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (div#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (div#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> p# minus(X, Y))
     (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> minus#(X, Y))
     (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> div#(minus(X, Y), s Y))}
    STATUS:
     arrows: 0.625000
     SCCS (2):
      Scc:
       {div#(s X, s Y) -> div#(minus(X, Y), s Y)}
      Scc:
       {minus#(s X, s Y) -> minus#(X, Y)}
      
      SCC (1):
       Strict:
        {div#(s X, s Y) -> div#(minus(X, Y), s Y)}
       Weak:
       {  minus(X, 0()) -> X,
        minus(s X, s Y) -> p minus(X, Y),
                  p s X -> X,
          div(0(), s Y) -> 0(),
          div(s X, s Y) -> s div(minus(X, Y), s Y)}
       Open
      
      SCC (1):
       Strict:
        {minus#(s X, s Y) -> minus#(X, Y)}
       Weak:
       {  minus(X, 0()) -> X,
        minus(s X, s Y) -> p minus(X, Y),
                  p s X -> X,
          div(0(), s Y) -> 0(),
          div(s X, s Y) -> s div(minus(X, Y), s Y)}
       Open