MAYBE
Time: 0.000775
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)}
  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